This is great news! When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it!
Some context, as not everybody may have heard about it.
Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver.
You can play with it online using its Lisp-like native language [2] or using the Python bindings [3]
The reason SMT is important is that several static analysis tools work by encoding the program constraints (such as pre/post conditions, invariants, ...) into a big formula. The satisfiability of this formula determines the correctness of the program, and sometimes assignments can be translated back to counterexamples to program correctness.
> When I was at MSR I heard the rumor that they wanted to sell Z3, not open-source it!
It has already been pointed out that they didn't open-source Z3, they just made the source code available under the same license the binary already was. I would add that they have been selling Z3 for a long time:
The limitation to non-commercial use means it's not quite 'open source' in the common meaning established by the Open Source Initiative. (Discrimination against a 'field of endeavor', such as business use, is not allowable under their definition.)
I think one of the problems with it not being true open source is that they are selling a commercial version @ the microsoft store for 14,950. I suspect this is why they choose this license.
I'd be interested if they would provide different terms for the source for the people that bought the commercial version, or if you would just be stuck with the binaries.
IMO it's still exciting. Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from.
And it means that it can be ported to platforms it's currently not available for.
That's excellent (good to learn from, shame it's only non commercial; it's a step forward though)! I was accidentally checking rise4fun for open source just last week. I hope they open source more; unfortunately the project I'm most curious about at the moment (quickcode) will not be open sourced as it is officially part of Excel now.
As a plain old programmer, would a tool like this be useful to me? How can I use a theorem prover to improve my code, or make it easier to write my code on a day to day basis? I've heard that Z3 is used for demonstrating security properties, how would I apply this to ensure my own systems are secure?
Wish someone would update the topic here, since it's not open source as per the generally understood definition ... (as the article's source has updated / corrected on his blog)
People bitching about MS misusing the term "open-source" are, IMO, ungrateful SOBs who have never attempted to implement a non-trivial algorithm based on nothing but a stack of academic papers.
For me, the greatest value in having the source is to learn from it, not to hijack it.
I think a lot of people appreciate the move MS made while simultaneously condemning them for their casual appropriation of a term having a well-established meaning. They've updated the blog post in the meantime, so this is a non-issue.
Resorting to ad-hominems does nothing to strengthen your argument, btw.
> Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose.
The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware.
> [A]ny feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential.
This I don't get. Why would MSFT want to publish confidential feedback?
> That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone's use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically. Upon any such termination, you shall destroy all of your copies of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this MSR-LA shall survive any termination of this MSR-LA.
This part I certainly understand. "Sue us and you can't use our toys anymore."
> That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make.
This, again, is unsurprising, but good to keep in mind.
The 'confidential feedback' boilerplate language would especially apply to projects with potential security implications. Your 'confidential feedback' might be disclosure of a security vulnerability and they'd want to choose to patch or not patch and publicly divulge or not divulge the vulnerability your feedback reveals.
The feedback thing is probably along the lines of not wanting to have to have internal controls to deal with confidential information in their feedback processing.
[+] [-] ot|13 years ago|reply
Some context, as not everybody may have heard about it.
Z3 is an SMT [1] solver. Since SMT generalizes SAT, it is clearly NP-hard, so a number of heuristics are needed. In particular, Z3 won several SMT speed competitions, so it has been for long the fastest SMT solver.
You can play with it online using its Lisp-like native language [2] or using the Python bindings [3]
The reason SMT is important is that several static analysis tools work by encoding the program constraints (such as pre/post conditions, invariants, ...) into a big formula. The satisfiability of this formula determines the correctness of the program, and sometimes assignments can be translated back to counterexamples to program correctness.
[1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
[2] http://rise4fun.com/Z3/bit-count
[3] http://rise4fun.com/Z3Py/nonlinear
[+] [-] olliesaunders|13 years ago|reply
[+] [-] pascal_cuoq|13 years ago|reply
It has already been pointed out that they didn't open-source Z3, they just made the source code available under the same license the binary already was. I would add that they have been selling Z3 for a long time:
http://www.microsoftstore.com/store/msstore/en_US/pd/product...
It has been there since 2011 according to my “archives”:
http://blog.frama-c.com/index.php?post/2011/12/23/Z3-in-Micr...
[+] [-] wiradikusuma|13 years ago|reply
[+] [-] gojomo|13 years ago|reply
[+] [-] lucian1900|13 years ago|reply
[+] [-] fredsanford|13 years ago|reply
:P
[+] [-] ajb|13 years ago|reply
[+] [-] sanxiyn|13 years ago|reply
[+] [-] jhartmann|13 years ago|reply
I'd be interested if they would provide different terms for the source for the people that bought the commercial version, or if you would just be stuck with the binaries.
Here is the link to buy the commercial version: http://www.microsoftstore.com/store/msstore/pd/Microsoft-Res...
[+] [-] jmartinpetersen|13 years ago|reply
[+] [-] wladimir|13 years ago|reply
And it means that it can be ported to platforms it's currently not available for.
[+] [-] tluyben2|13 years ago|reply
[+] [-] subleq|13 years ago|reply
[+] [-] contextfree|13 years ago|reply
[+] [-] timtadh|13 years ago|reply
[+] [-] apawloski|13 years ago|reply
[+] [-] zvrba|13 years ago|reply
For me, the greatest value in having the source is to learn from it, not to hijack it.
[+] [-] algorias|13 years ago|reply
Resorting to ad-hominems does nothing to strengthen your argument, btw.
[+] [-] elviejo|13 years ago|reply
[+] [-] derleth|13 years ago|reply
> Microsoft is granted back, without any restrictions or limitations, a non-exclusive, perpetual, irrevocable, royalty-free, assignable and sub-licensable license, to reproduce, publicly perform or display, install, use, modify, post, distribute, make and have made, sell and transfer your modifications to and/or derivative works of the Software source code or data, for any purpose.
The above I can understand. MSFT claims ownership of any modifications you make to its software. Be aware.
> [A]ny feedback about the Software provided by you to us is voluntarily given, and Microsoft shall be free to use the feedback as it sees fit without obligation or restriction of any kind, even if the feedback is designated by you as confidential.
This I don't get. Why would MSFT want to publish confidential feedback?
> That if you breach this MSR-LA or if you sue anyone over patents that you think may apply to or read on the Software or anyone's use of the Software, this MSR-LA (and your license and rights obtained herein) terminate automatically. Upon any such termination, you shall destroy all of your copies of the Software immediately. Sections 3, 4, 5, 6, 7, 8, 11 and 12 of this MSR-LA shall survive any termination of this MSR-LA.
This part I certainly understand. "Sue us and you can't use our toys anymore."
> That the patent rights, if any, granted to you in this MSR-LA only apply to the Software, not to any derivative works you make.
This, again, is unsurprising, but good to keep in mind.
[+] [-] nwatson|13 years ago|reply
[+] [-] andrewaylett|13 years ago|reply
[+] [-] sadga|13 years ago|reply
MSFT claims a non-exclusive right to use your modifications.