Could this be used to tes ZED models?
The Z3 theorem prover is now open source
31–40 of 77 posts
Re: The Z3 theorem prover is now open source
#32Earlier quoted context omitted.
> Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. The GPL has a few problems, but non-commercial causes are just noxious. Who exactly can use a non-commercial piece of software? Presumably, universities can. Can a government research lab use it? How about a military research lab? What about a contractor doing military R&D? If Exon-Mobile uses this to search for oil, is this…
Actually, interpreted code or browser code isn't really ambiguous. GPL is based on "derivative works" not necessarily C-style linking.
Is progressive enhancement of a HTML page enough to make the rest of the frontend "derivative"? What about the backend? What if they interact?
If the JS engine mixes interpreted code with the proprietary DOM, how does that work?
How about LGPL works?
But you're right - it's usually pretty clear if you think about it. There will always be edge-cases, but unlike non-commercial clauses the edge cases aren't that common.
Re: The Z3 theorem prover is now open source
#33I 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.
Here is the link to buy the commercial version: http://www.microsoftstore.com/store/msstore/pd/Microsoft-Res...
Re: The Z3 theorem prover is now open source
#34From 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…
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.
Re: The Z3 theorem prover is now open source
#35Earlier quoted context omitted.
It's not open source by any stretch of the imagination. The Microsoft blog is quite simply lying.
Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.
GPL has no restrictions at all on commercial use and in commercial use places no obligations on you at all.
If you distribute GPL code you then become subject to its restrictions and must provide the code.
Re: The Z3 theorem prover is now open source
#36Earlier quoted context omitted.
Or the poster doesn't understand what open source really is, or their definition of open source is different from yours. Honestly, GPL screws up commercial use almost as much as a non commercial use restrictions. But I totally agree that open source are not the right words to use in this situation. Full disclosure, I work for Microsoft.
GPL has no restrictions at all on commercial use and in commercial use places no obligations on you at all. If you distribute GPL code you then become subject to its restrictions and must provide the code.
Sure, I'm aware of this. My point was that GPL is almost as poisonous as a non commercial use restriction in terms of distributing software. GPL works great on the server where this isn't a concern, but doesn't work for almost any other commercial use case. Very arbitrary but at least very clear.
Re: The Z3 theorem prover is now open source
#37Earlier quoted context omitted.
Open Source a term with a single, specific definition. It is damaging to the ideas of FLOSS to allow stuff like "shared source" to be called open source. EDIT: Removed reference to "open source" being trademarked, it is in fact not, apologies for the confusion.
No. This is a fantasy. A trademark does not take ownership of general words or phrases from the people.
A trademark does not take ownership of general words or phrases from the people.
Except when that trademark is "Windows" or "Office" or "Word".
Re: The Z3 theorem prover is now open source
#38The 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.
Those bastards. How dare they publish their source code on terms we don't agree with.
Re: The Z3 theorem prover is now open source
#39This 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-l…
what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.
Solvers are somewhat popular in software security, both for automatically uncovering invariants (and exploitable lack of invariants), and also for modeling program binaries and solving for collections of basic blocks that can executed during a memory corruption attack to accomplish attacker goals.
Re: The Z3 theorem prover is now open source
#40Earlier quoted context omitted.
Why do you think they are "simply lying", rather than (for example) being simply mistaken?
Because they've been trying to dilute the term "open source" for quite a while now.
1997 called and &c &c. Microsoft could give a shit about damaging "open source".