The Z3 theorem prover is now open source
research.microsoft.com
The Z3 theorem prover is now open source
1–10 of 77 posts
Re: The Z3 theorem prover is now open source
#2The 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.)
Re: The Z3 theorem prover is now open source
#3It seemed really exciting until I realized that it is only available for non-commercial purposes.
Re: The Z3 theorem prover is now open source
#4This 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.
[1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
Re: The Z3 theorem prover is now open source
#5Non-commercial only. There are several similar projects some of which are really open source: http://smtlib.cs.uiowa.edu/solvers.html
Re: The Z3 theorem prover is now open source
#6It seemed really exciting until I realized that it is only available for non-commercial purposes.
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.
Re: The Z3 theorem prover is now open source
#7The 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.)
The no commercial use thing is Microsoft speak for "We couldn't figure out how to make money with it, but if you do, give it to me."
:P
Re: The Z3 theorem prover is now open source
#8The 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.)
It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.
Re: The Z3 theorem prover is now open source
#9It seemed really exciting until I realized that it is only available for non-commercial purposes.
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.
> Sure, you cannot use it directly for commercial purposes, but having the source for something like this is great to learn from.
As long as nobody sees you, otherwise you are vulnerable to a lawsuit. If I had serious plans to make my own implementation I would purposefully avoid even running this program.
Re: The Z3 theorem prover is now open source
#10From the license text:
> 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.