7 ms·

The Z3 Theorem Prover released under MIT license

304 points by dahlia 12y ago

tluyben2 12y ago
Great project by MS research: good to see they picked a great license! See http://rise4fun.com http://rise4fun.com for more great projects like that.
pavpanchekha 12y ago
I'm working with Z3 now, and it's been a real joy. One of the biggest advances in programming languages in recent years, perhaps. Glad to see it open-sourced and moved to Github.
- pradn 12y ago
  What do you use it for?
  - LeonRobrotsky 12y ago
    Making vague but supportive comments on HN.
    - pavpanchekha 12y ago
      I had a long day at work, and didn't see this. I posted another comment (couldn't edit; too late). You may be sure that I am MS shill, cleverly astroturfing their now-free product.
      - LeonRobrotsky 12y ago
        Sorry- my remark wasn't intended as a shill accusation, but re-reading it now, I see it. It was tongue-in-cheek, I enjoyed the positivity in your original comment.
  - ufo 12y ago
    SAT solvers and SMT solvers are greeat for the kind of problems where your first thought would be to use brute force or backtracking. They use some really clever implementation tricks and heuristics that are likely to beat any of your algorithms that you write from scratch. One of the more famous places where these constraint solvers are used is to deal with dependency management in package systems. For example, zeroinstall uses a SAT solver to resolve dependency conflicts. http://0install.net/solver.html http://0install.net/solver.html A sillier example is the time I used a sat solver to find the solutions for a flash puzzle game. The part I'm proudest of is that the sat solver could handle the highly symmetric cases that stumped the hand-written backtracking algorithms. And if I had used an SMT solver instead of SAT I would not have had to convert everything all the way doen to boolean formulas. https://github.com/hugomg/hexiom https://github.com/hugomg/hexiom In the readme I explain a bit why the sat solver helped.
    - david-given 12y ago
      Hmm. Would a SAT solver be useful for compiler technologies? A compiler is basically solving the problem of: here is a sequence of things I want done; here is a description of what the machine can do; find a combination of the latter which achieves the former. The details are the tricky bit, particularly for unpleasantly asymmetric instruction sets like the old 8-bit architectures. It would be so nice if I could just throw a description of the problem at some sort of machine reasoning system and have it Just Work...
      - TheLoneWolfling 12y ago
        There are superoptimizers that do exactly that. But current SAT solvers aren't powerful enough to do so at much more than a few tens of instructions long. Still useful though.
      - bronxbomber92 12y ago
        Check out Alive http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 https://github.com/nunoplopes/alive https://github.com/nunoplopes/alive http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170
- andrepd 12y ago
  Can you elaborate on what exactly do you do with it, and how?
  - microarchitect 12y ago
    I am not the OP, but I'm using Z3 in my research to help with the formal verification of hardware and firmware. My problem is as follows. I have a microcontroller which runs firmware. I want to verify various things about the hardware+firmware combination. For instance, I may be interested in proving that user mode firmware cannot change the MMU configuration. There are many parts to this problem. First is verifying that the kernel doesn't expose routines that let you do these kinds of things. This is a kind of s/w verification problem, somewhat well studied. Second, you want to make sure there are no h/w bugs in the microcontroller itself which the user mode software can exploit to do bad stuff. This is traditional h/w verification, also well-studied. The third is that there aren't weird corners of the microcontroller ISA specification itself which can be exploited. This is also a kind of h/w bug albeit a specification bug. The third part is where Z3 comes in because often, there isn't any specification, and if there is, it's a bunch of PDFs or word documents. What we want is to generate a formal specification, which you can examine using formal tools to prove that it satisfies certain properties. And then we want to prove that our implementation conforms to this specification. We're using some techniques from program synthesis with Z3 as the solver for this.
    - asb 12y ago
      Hi, I can't see an email address in your profile so sorry for the public message. With the lowRISC project http://lowrisc.org/ http://lowrisc.org/ and related research at University of Cambridge we're becoming very interested in formal verification of hw+sw. I found this work out of Kaiserslautern interesting <http://www-eda.eit.uni-kl.de/eis/research/publications/papers/DAC2011.pdf> http://www-eda.eit.uni-kl.de/eis/research/publications/paper.... Could you say any more about your research? I'd be very interested in an email conversation - I'm at alex.bradbury@cl.cam.ac.uk
  - tokenrove 12y ago
    One of my favorite uses is concolic testing which has really been enabled by SMT solvers (of which Z3 is one of the best): http://en.wikipedia.org/wiki/Concolic_testing http://en.wikipedia.org/wiki/Concolic_testing Check out MS's Code Digger, which uses Z3 as well: http://research.microsoft.com/en-us/projects/codedigger/ http://research.microsoft.com/en-us/projects/codedigger/
- pavpanchekha 12y ago
  Long day at work, didn't see the thread that grew out of this comment. What do I use Z3 for? Right now, I'm implementing a web browser in Z3 so that Z3 can solve CSS layout queries. Like, "write me a CSS file given this website mockup". But honestly, it's just damn fun to play with, and especially for solving small logic puzzles. For example, a friend and I were playing a board game where each player had hit points, which they represented with two types of cards: type A had "5" on one side and "1" on the other, and type B had a "20" on one side and a "10" on the other. You'd represent your current hitpoints by displaying some number of these cards (out of 6 of the first type and 3 of the second type) face up, and adding up the totals. So, I wanted to find out: what's the smallest hit point value that I can't represent with some combination of cards? The traditional mathematical approach would be generating functions, but that would require at least pencil and paper. With Z3, I execute: (declare-const a1 Int) (declare-const a2 Int) (declare-const a3 Int) (declare-const a4 Int) (declare-const a5 Int) (declare-const a6 Int) (declare-const b1 Int) (declare-const b2 Int) (declare-const b3 Int) (assert (or (= a1 0) (= a1 1) (= a1 5))) (assert (or (= a2 0) (= a2 1) (= a2 5))) (assert (or (= a3 0) (= a3 1) (= a3 5))) (assert (or (= a4 0) (= a4 1) (= a4 5))) (assert (or (= a5 0) (= a5 1) (= a5 5))) (assert (or (= a6 0) (= a6 1) (= a6 5))) (assert (or (= b1 0) (= b1 10) (= b1 20))) (assert (or (= b2 0) (= b2 10) (= b2 20))) (assert (or (= b3 0) (= b3 10) (= b3 20))) (assert (= (+ a1 a2 a3 a4 a5 a6 b1 b2 b3) i)) (check-sat))))))) If you run this for different values of i (using push and pop if you're clever; I just called Z3 100 times), you can get a "sat" or "unsat" which tells you whether a particular total is reachable.
1ris 12y ago
This is really huge. Maybe Idris or Coq integrate Z3.
- javra 12y ago
  One of the main devs of Z3, Leonardo de Moura, is acutally working on a new, dependently typed, theorem prover called "Lean": http://leanprover.github.io/ http://leanprover.github.io/
  - NotableAlamode 12y ago
    Is Lean an LCF system or Curry-Howard based? It seems to be the latter, but if so, what's it's main advantage over the many other Curry-Howard based systems?
- CHY872 12y ago
  Coq already could, if they wanted to. Z3 supports the SMT-Lib format, which means that any theorem prover that can both output that and execute a shell command can invoke Z3. This has no bearing on Z3's specific license, unless you want to use that tool for commercial purposes. For an example of this being used in a similar tool to Coq, Isabelle/HOL's 'Sledgehammer' tactic will attempt to use Z3 (and then reconstruct a proof) where its own solvers fail. It's all pretty nifty! http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.306.6424&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.306... HOL4 also has Z3 (and Yices) support, but I think the Z3 support is a little out of date (in particular, it errors immediately on start).
- NotableAlamode 12y ago
  Idris and Coq are based on the Curry-Howard correspondence. That makes it difficult / impossible to integrate Z3, because Z3 in general does not output concrete proofs. More precisely, some Z3 modules can output proof objects, but not all. There is work on integrating Z3 with LCF-style provers like Isabelle [1]. There is also active work on Z3 integration with Coq, although I'm not sure how this works. See [2] for a brief discussion of these issues by one of the Z3 authors. [1] http://www21.in.tum.de/~boehmes/proofrec.pdf http://www21.in.tum.de/~boehmes/proofrec.pdf [2] http://stackoverflow.com/questions/11531589/difference-between-z3-and-coq http://stackoverflow.com/questions/11531589/difference-betwe...
tsomctl 12y ago
Note that the Z3 source code has been available for a while, but a commercial license was $10,000.
- Drakim 12y ago
  I wonder who bought the last license, and how long since it now became free to use.
  - CHY872 12y ago
    I suspect that they've sold a fair few licenses in their time. SMT solvers are widely used in industry, and to my knowledge Z3 is one of the better ones. It's probably just that the volume of sales isn't going to make sense when comparing to the size of the team.
- wslh 12y ago
  $ 10,000 seems like a magic number. Another Microsoft Research project, Detours [1] costs $ 9,999.95. [1] http://www.microsoftstore.com/store/msus/en_AU/pdp/Microsoft-Research-Detours-v3-Professional/productID.254378300 http://www.microsoftstore.com/store/msus/en_AU/pdp/Microsoft...
  - raverbashing 12y ago
    Yes It's cheap enough for a company to buy it without many signatures, but also on the upper scale of what people who "don't want Open Source" can pay.
harperlee 12y ago
Could please someone informed explain how is this more restricted to only prove theorems, instead of being a more general prolog-like system? From the Microsoft Research page, I read: > Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. And with my current knowledge (which is low on the matter) I can't reconcile arithmetic, arrays, quantifiers, etc. with general program verification...
- ufo 12y ago
  It might be better to see Ze and other SMT solvers as souped up SAT solvers instead of comparing them to general theorem provers. The neat thing about Z3 is that it has efficient solvers for the more specific subproblems (linear programming, bit vectors, etc) that you can't have if you state everything using "general" constraint programming. At the same time, Z3 lets you work at a higher level of abstraction - for example, you can reason about bit verctors or arithmetic directly instead of having to encode it with boolean formulas.
- eslaught 12y ago
  Z3 is an SMT solver (https://en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories). You can think of it like a SAT solver with extra optimizations for certain domains, so that it doesn't need to do bit-blasting to e.g. compare integers. SMT is NP-complete, just like SAT, but it is decidable (so the solver will "eventually" give you a yes/no answer, though "eventually" could be a long time). This is in pretty stark contrast to Prolog, which includes features which make it undecidable. Therefore you can make Prolog loop infinitely, while that is not possible in an SMT solver.
  - poizan42 12y ago
    Uhm you can throw diophantine equations after Z3 which certainly isn't a decideable problem. I have no idea whether it errs on the side of termination (i.e. not giving an answer) or non-termination (i.e. running forever).
frik 12y ago
I heard Microsoft uses provers to check (automated verification) third party kernel mode device drivers. Is that the Z3 proofer? I searched on Google and got several results but the meaning of the term "kernel" is overloaded and means different things in operating systems and proofers/solvers.
- tedks 12y ago
  This is the project webpage, though I can't recall if it uses Z3 or not: http://research.microsoft.com/en-us/projects/slam/ http://research.microsoft.com/en-us/projects/slam/
  - frik 12y ago
    Thanks. From that page: Pointers in SLAM2: Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2
- ufo 12y ago
  When people talk about kernels it has more to do with proof verification. Once you have written down a proof for something you need a way to verify is the proof is correct, checking for syntax errors, checking if each step is a valid inference step, etc. For the more advanced theorem provers what they tend to try to do is use a comlpex system to let the programmer build a proof thats easy to describe but in the end convert it to a longer proof that a simpler verifier can check. As for Z3, its strength is about contraint solving. You can specify a set of constraints and it will try to find if there is a viable solution that satisfies the constraints. It includes a SAT (boolean satisfiability)solver and beefs it up with support for some higher level things, like integer arithmetic, bit vectors, etc. This kind of constraint solver is very useful for finding bugs: for example, the notorious intel floating point bug was found out by asking a SAT solver to find an input where the processor's circuit produced the wrong value.
- jonjacky 12y ago
  This page says that the driver verifier uses the SLAM verification engine - I am not sure whether/how that is related to Z3: http://research.microsoft.com/en-us/projects/slam/ http://research.microsoft.com/en-us/projects/slam/
hokkos 12y ago
I hope they will open source Microsoft.Automata too, it was very useful for a project where I had to generate samples of strings that had to conform to multiple regex : http://research.microsoft.com/en-us/projects/automata/ http://research.microsoft.com/en-us/projects/automata/
- porges 12y ago
  There are potentially patents on the code, e.g. https://www.google.co.nz/patents/US8515891 https://www.google.co.nz/patents/US8515891 which discusses PEX + regex (mentioning SMT solvers).
panic 12y ago
For one example of why Z3 is cool, check out this application to "peephole" compiler optimizations: http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170 Also take a look at the "licensing" section to see why switching to the MIT license is a big deal. Even open source software projects like LLVM have had to worry about whether using Z3 was OK or not. Now they don't any more!
bbcbasic 12y ago
I wonder, does Code Contracts use Z3?
- ygra 12y ago
  Code Contracts are just assertions. Pex can use them though and is built on Z3, iirc.
  - bbcbasic 12y ago
    They seem to be more than assertions. You get warnings at build time and clearly some proving engine must be in use.
fit2rule 12y ago
Could someone who knows about these things, compare Z3 with the Google or-tools? (https://code.google.com/p/or-tools/ https://code.google.com/p/or-tools/) Pro's/Con's of the two?
tomp 12y ago
Amazing! When I was prototyping a programming language with support for contracts (or refined types, e.g. `x : int if x > 0`), I tested a few different SMT solvers, including AltErgo, CVC and Yices (these seemed to be the most used open source solvers). However, none of them were nearly as useful as Z3. In particular, they had no concept of a stack that allows the user to define different assertions locally, and then cancel them later. Without the stack, one would need to restart the solver and re-declare all variables (with all their constraints) for every function call with a constraint, compared to a single SMT script for each function verified in Z3. Also, Z3 supports much more theories, in particular it supports non-linear integer arithmetics (which is an undecidable, incomplete theory), either by using some heuristics, or by translating the statements into the theory of real arithmetics (which is complete and decidable).
cjdrake 12y ago
This is a really great library. Thanks to Microsoft :).
jrapdx3 12y ago
z3 is something I didn't know about until encountering it here. Spent the last few hours playing with the solver, it's quite interesting especially since I've had a fair amount of exposure to Scheme. Felt right at home after getting it up and running. Glitch-free compiling and installing under FreeBSD. The only problem was finding documentation. Rise4fun.com is mentioned in another post, the exact URL for getting started is http://rise4fun.com/Z3/tutorial/guide http://rise4fun.com/Z3/tutorial/guide. Also, very useful information here-- http://www.smt-lib.org/ http://www.smt-lib.org/
csl 12y ago
I've used model checkers before, but never SMT solvers. Looks really cool! Anyway, here's a great post on solving a Project Euler problem using Z3/SMT-lib, which may be inspiring for other novices like myself: http://blogs.teamb.com/craigstuntz/2014/07/07/38818/ http://blogs.teamb.com/craigstuntz/2014/07/07/38818/
fugyk 12y ago
You can try Z3 online here: http://rise4fun.com/Z3/ http://rise4fun.com/Z3/

304 points by dahlia 12y ago

Great project by MS research: good to see they picked a great license! See http://rise4fun.com http://rise4fun.com for more great projects like that.

pavpanchekha 12y ago

I'm working with Z3 now, and it's been a real joy. One of the biggest advances in programming languages in recent years, perhaps. Glad to see it open-sourced and moved to Github.

pradn 12y ago
What do you use it for?
- LeonRobrotsky 12y ago
  Making vague but supportive comments on HN.
  - pavpanchekha 12y ago
    I had a long day at work, and didn't see this. I posted another comment (couldn't edit; too late). You may be sure that I am MS shill, cleverly astroturfing their now-free product.
    - LeonRobrotsky 12y ago
      Sorry- my remark wasn't intended as a shill accusation, but re-reading it now, I see it. It was tongue-in-cheek, I enjoyed the positivity in your original comment.
- ufo 12y ago
  SAT solvers and SMT solvers are greeat for the kind of problems where your first thought would be to use brute force or backtracking. They use some really clever implementation tricks and heuristics that are likely to beat any of your algorithms that you write from scratch. One of the more famous places where these constraint solvers are used is to deal with dependency management in package systems. For example, zeroinstall uses a SAT solver to resolve dependency conflicts. http://0install.net/solver.html http://0install.net/solver.html A sillier example is the time I used a sat solver to find the solutions for a flash puzzle game. The part I'm proudest of is that the sat solver could handle the highly symmetric cases that stumped the hand-written backtracking algorithms. And if I had used an SMT solver instead of SAT I would not have had to convert everything all the way doen to boolean formulas. https://github.com/hugomg/hexiom https://github.com/hugomg/hexiom In the readme I explain a bit why the sat solver helped.
  - david-given 12y ago
    Hmm. Would a SAT solver be useful for compiler technologies? A compiler is basically solving the problem of: here is a sequence of things I want done; here is a description of what the machine can do; find a combination of the latter which achieves the former. The details are the tricky bit, particularly for unpleasantly asymmetric instruction sets like the old 8-bit architectures. It would be so nice if I could just throw a description of the problem at some sort of machine reasoning system and have it Just Work...
    - TheLoneWolfling 12y ago
      There are superoptimizers that do exactly that. But current SAT solvers aren't powerful enough to do so at much more than a few tens of instructions long. Still useful though.
    - bronxbomber92 12y ago
      Check out Alive http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 http://web.ist.utl.pt/nuno.lopes/pubs.php?id=alive-pldi15 https://github.com/nunoplopes/alive https://github.com/nunoplopes/alive http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170
andrepd 12y ago
Can you elaborate on what exactly do you do with it, and how?
- microarchitect 12y ago
  I am not the OP, but I'm using Z3 in my research to help with the formal verification of hardware and firmware. My problem is as follows. I have a microcontroller which runs firmware. I want to verify various things about the hardware+firmware combination. For instance, I may be interested in proving that user mode firmware cannot change the MMU configuration. There are many parts to this problem. First is verifying that the kernel doesn't expose routines that let you do these kinds of things. This is a kind of s/w verification problem, somewhat well studied. Second, you want to make sure there are no h/w bugs in the microcontroller itself which the user mode software can exploit to do bad stuff. This is traditional h/w verification, also well-studied. The third is that there aren't weird corners of the microcontroller ISA specification itself which can be exploited. This is also a kind of h/w bug albeit a specification bug. The third part is where Z3 comes in because often, there isn't any specification, and if there is, it's a bunch of PDFs or word documents. What we want is to generate a formal specification, which you can examine using formal tools to prove that it satisfies certain properties. And then we want to prove that our implementation conforms to this specification. We're using some techniques from program synthesis with Z3 as the solver for this.
  - asb 12y ago
    Hi, I can't see an email address in your profile so sorry for the public message. With the lowRISC project http://lowrisc.org/ http://lowrisc.org/ and related research at University of Cambridge we're becoming very interested in formal verification of hw+sw. I found this work out of Kaiserslautern interesting <http://www-eda.eit.uni-kl.de/eis/research/publications/papers/DAC2011.pdf> http://www-eda.eit.uni-kl.de/eis/research/publications/paper.... Could you say any more about your research? I'd be very interested in an email conversation - I'm at alex.bradbury@cl.cam.ac.uk
- tokenrove 12y ago
  One of my favorite uses is concolic testing which has really been enabled by SMT solvers (of which Z3 is one of the best): http://en.wikipedia.org/wiki/Concolic_testing http://en.wikipedia.org/wiki/Concolic_testing Check out MS's Code Digger, which uses Z3 as well: http://research.microsoft.com/en-us/projects/codedigger/ http://research.microsoft.com/en-us/projects/codedigger/
pavpanchekha 12y ago
Long day at work, didn't see the thread that grew out of this comment. What do I use Z3 for? Right now, I'm implementing a web browser in Z3 so that Z3 can solve CSS layout queries. Like, "write me a CSS file given this website mockup". But honestly, it's just damn fun to play with, and especially for solving small logic puzzles. For example, a friend and I were playing a board game where each player had hit points, which they represented with two types of cards: type A had "5" on one side and "1" on the other, and type B had a "20" on one side and a "10" on the other. You'd represent your current hitpoints by displaying some number of these cards (out of 6 of the first type and 3 of the second type) face up, and adding up the totals. So, I wanted to find out: what's the smallest hit point value that I can't represent with some combination of cards? The traditional mathematical approach would be generating functions, but that would require at least pencil and paper. With Z3, I execute: (declare-const a1 Int) (declare-const a2 Int) (declare-const a3 Int) (declare-const a4 Int) (declare-const a5 Int) (declare-const a6 Int) (declare-const b1 Int) (declare-const b2 Int) (declare-const b3 Int) (assert (or (= a1 0) (= a1 1) (= a1 5))) (assert (or (= a2 0) (= a2 1) (= a2 5))) (assert (or (= a3 0) (= a3 1) (= a3 5))) (assert (or (= a4 0) (= a4 1) (= a4 5))) (assert (or (= a5 0) (= a5 1) (= a5 5))) (assert (or (= a6 0) (= a6 1) (= a6 5))) (assert (or (= b1 0) (= b1 10) (= b1 20))) (assert (or (= b2 0) (= b2 10) (= b2 20))) (assert (or (= b3 0) (= b3 10) (= b3 20))) (assert (= (+ a1 a2 a3 a4 a5 a6 b1 b2 b3) i)) (check-sat))))))) If you run this for different values of i (using push and pop if you're clever; I just called Z3 100 times), you can get a "sat" or "unsat" which tells you whether a particular total is reachable.

1ris 12y ago

This is really huge. Maybe Idris or Coq integrate Z3.

javra 12y ago
One of the main devs of Z3, Leonardo de Moura, is acutally working on a new, dependently typed, theorem prover called "Lean": http://leanprover.github.io/ http://leanprover.github.io/
- NotableAlamode 12y ago
  Is Lean an LCF system or Curry-Howard based? It seems to be the latter, but if so, what's it's main advantage over the many other Curry-Howard based systems?
CHY872 12y ago
Coq already could, if they wanted to. Z3 supports the SMT-Lib format, which means that any theorem prover that can both output that and execute a shell command can invoke Z3. This has no bearing on Z3's specific license, unless you want to use that tool for commercial purposes. For an example of this being used in a similar tool to Coq, Isabelle/HOL's 'Sledgehammer' tactic will attempt to use Z3 (and then reconstruct a proof) where its own solvers fail. It's all pretty nifty! http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.306.6424&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.306... HOL4 also has Z3 (and Yices) support, but I think the Z3 support is a little out of date (in particular, it errors immediately on start).
NotableAlamode 12y ago
Idris and Coq are based on the Curry-Howard correspondence. That makes it difficult / impossible to integrate Z3, because Z3 in general does not output concrete proofs. More precisely, some Z3 modules can output proof objects, but not all. There is work on integrating Z3 with LCF-style provers like Isabelle [1]. There is also active work on Z3 integration with Coq, although I'm not sure how this works. See [2] for a brief discussion of these issues by one of the Z3 authors. [1] http://www21.in.tum.de/~boehmes/proofrec.pdf http://www21.in.tum.de/~boehmes/proofrec.pdf [2] http://stackoverflow.com/questions/11531589/difference-between-z3-and-coq http://stackoverflow.com/questions/11531589/difference-betwe...

tsomctl 12y ago

Note that the Z3 source code has been available for a while, but a commercial license was $10,000.

Drakim 12y ago
I wonder who bought the last license, and how long since it now became free to use.
- CHY872 12y ago
  I suspect that they've sold a fair few licenses in their time. SMT solvers are widely used in industry, and to my knowledge Z3 is one of the better ones. It's probably just that the volume of sales isn't going to make sense when comparing to the size of the team.
wslh 12y ago
$ 10,000 seems like a magic number. Another Microsoft Research project, Detours [1] costs $ 9,999.95. [1] http://www.microsoftstore.com/store/msus/en_AU/pdp/Microsoft-Research-Detours-v3-Professional/productID.254378300 http://www.microsoftstore.com/store/msus/en_AU/pdp/Microsoft...
- raverbashing 12y ago
  Yes It's cheap enough for a company to buy it without many signatures, but also on the upper scale of what people who "don't want Open Source" can pay.

harperlee 12y ago

Could please someone informed explain how is this more restricted to only prove theorems, instead of being a more general prolog-like system? From the Microsoft Research page, I read: > Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. And with my current knowledge (which is low on the matter) I can't reconcile arithmetic, arrays, quantifiers, etc. with general program verification...

ufo 12y ago
It might be better to see Ze and other SMT solvers as souped up SAT solvers instead of comparing them to general theorem provers. The neat thing about Z3 is that it has efficient solvers for the more specific subproblems (linear programming, bit vectors, etc) that you can't have if you state everything using "general" constraint programming. At the same time, Z3 lets you work at a higher level of abstraction - for example, you can reason about bit verctors or arithmetic directly instead of having to encode it with boolean formulas.
eslaught 12y ago
Z3 is an SMT solver (https://en.wikipedia.org/wiki/Satisfiability_modulo_theories https://en.wikipedia.org/wiki/Satisfiability_modulo_theories). You can think of it like a SAT solver with extra optimizations for certain domains, so that it doesn't need to do bit-blasting to e.g. compare integers. SMT is NP-complete, just like SAT, but it is decidable (so the solver will "eventually" give you a yes/no answer, though "eventually" could be a long time). This is in pretty stark contrast to Prolog, which includes features which make it undecidable. Therefore you can make Prolog loop infinitely, while that is not possible in an SMT solver.
- poizan42 12y ago
  Uhm you can throw diophantine equations after Z3 which certainly isn't a decideable problem. I have no idea whether it errs on the side of termination (i.e. not giving an answer) or non-termination (i.e. running forever).

frik 12y ago

I heard Microsoft uses provers to check (automated verification) third party kernel mode device drivers. Is that the Z3 proofer? I searched on Google and got several results but the meaning of the term "kernel" is overloaded and means different things in operating systems and proofers/solvers.

tedks 12y ago
This is the project webpage, though I can't recall if it uses Z3 or not: http://research.microsoft.com/en-us/projects/slam/ http://research.microsoft.com/en-us/projects/slam/
- frik 12y ago
  Thanks. From that page: Pointers in SLAM2: Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2
ufo 12y ago
When people talk about kernels it has more to do with proof verification. Once you have written down a proof for something you need a way to verify is the proof is correct, checking for syntax errors, checking if each step is a valid inference step, etc. For the more advanced theorem provers what they tend to try to do is use a comlpex system to let the programmer build a proof thats easy to describe but in the end convert it to a longer proof that a simpler verifier can check. As for Z3, its strength is about contraint solving. You can specify a set of constraints and it will try to find if there is a viable solution that satisfies the constraints. It includes a SAT (boolean satisfiability)solver and beefs it up with support for some higher level things, like integer arithmetic, bit vectors, etc. This kind of constraint solver is very useful for finding bugs: for example, the notorious intel floating point bug was found out by asking a SAT solver to find an input where the processor's circuit produced the wrong value.
jonjacky 12y ago
This page says that the driver verifier uses the SLAM verification engine - I am not sure whether/how that is related to Z3: http://research.microsoft.com/en-us/projects/slam/ http://research.microsoft.com/en-us/projects/slam/

hokkos 12y ago

I hope they will open source Microsoft.Automata too, it was very useful for a project where I had to generate samples of strings that had to conform to multiple regex : http://research.microsoft.com/en-us/projects/automata/ http://research.microsoft.com/en-us/projects/automata/

porges 12y ago
There are potentially patents on the code, e.g. https://www.google.co.nz/patents/US8515891 https://www.google.co.nz/patents/US8515891 which discusses PEX + regex (mentioning SMT solvers).

panic 12y ago

For one example of why Z3 is cool, check out this application to "peephole" compiler optimizations: http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170 Also take a look at the "licensing" section to see why switching to the MIT license is a big deal. Even open source software projects like LLVM have had to worry about whether using Z3 was OK or not. Now they don't any more!

bbcbasic 12y ago

I wonder, does Code Contracts use Z3?

ygra 12y ago
Code Contracts are just assertions. Pex can use them though and is built on Z3, iirc.
- bbcbasic 12y ago
  They seem to be more than assertions. You get warnings at build time and clearly some proving engine must be in use.

fit2rule 12y ago

Could someone who knows about these things, compare Z3 with the Google or-tools? (https://code.google.com/p/or-tools/ https://code.google.com/p/or-tools/) Pro's/Con's of the two?

tomp 12y ago

Amazing! When I was prototyping a programming language with support for contracts (or refined types, e.g. `x : int if x > 0`), I tested a few different SMT solvers, including AltErgo, CVC and Yices (these seemed to be the most used open source solvers). However, none of them were nearly as useful as Z3. In particular, they had no concept of a stack that allows the user to define different assertions locally, and then cancel them later. Without the stack, one would need to restart the solver and re-declare all variables (with all their constraints) for every function call with a constraint, compared to a single SMT script for each function verified in Z3. Also, Z3 supports much more theories, in particular it supports non-linear integer arithmetics (which is an undecidable, incomplete theory), either by using some heuristics, or by translating the statements into the theory of real arithmetics (which is complete and decidable).

cjdrake 12y ago

This is a really great library. Thanks to Microsoft :).

jrapdx3 12y ago

z3 is something I didn't know about until encountering it here. Spent the last few hours playing with the solver, it's quite interesting especially since I've had a fair amount of exposure to Scheme. Felt right at home after getting it up and running. Glitch-free compiling and installing under FreeBSD. The only problem was finding documentation. Rise4fun.com is mentioned in another post, the exact URL for getting started is http://rise4fun.com/Z3/tutorial/guide http://rise4fun.com/Z3/tutorial/guide. Also, very useful information here-- http://www.smt-lib.org/ http://www.smt-lib.org/

csl 12y ago

I've used model checkers before, but never SMT solvers. Looks really cool! Anyway, here's a great post on solving a Project Euler problem using Z3/SMT-lib, which may be inspiring for other novices like myself: http://blogs.teamb.com/craigstuntz/2014/07/07/38818/ http://blogs.teamb.com/craigstuntz/2014/07/07/38818/

fugyk 12y ago

You can try Z3 online here: http://rise4fun.com/Z3/ http://rise4fun.com/Z3/