Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Z3: A high-performance theorem prover from Microsoft Research

z3.codeplex.com

Post reply on HN
Print view View original

31–40 of 50 posts

Re: Z3: A high-performance theorem prover from Microsoft Research

#31

Post by psuter »

colanderman wrote: post #17
tptacek wrote: post #15

If people are using this for interesting projects, I'd love some details.

Last week I wrote a fun tool using it (actually, any SMT-LIB 2 compatible solver, of which Z3 seems to be the only open-source-ish one that works out of the box) to search for optimal branch-free load-free C implementations of small integer lookup tables (i.e. something the compiler should do but doesn't). It's really a minimal use of an SMT solver, but it saved me from having to think of a more clever algorithm than…

In case you or someone else is still looking, CVC4 [1] is a competitive open source alternative to Z3 or Yices.

[1] http://cvc4.cs.nyu.edu/

Re: Z3: A high-performance theorem prover from Microsoft Research

#32

Post by tel »

shirkey wrote: post #30

What are the advantages/differences between this and Google's or-tools ( https://code.google.com/p/or-tools/ ), which is available under Apache license?

Without examining or-tools too much, I think it's solving a totally different problem. The Z3 guideis a good way to learn more (http://rise4fun.com/z3/tutorial)

Re: Z3: A high-performance theorem prover from Microsoft Research

#33

Post by psuter »

tptacek wrote: post #15

If people are using this for interesting projects, I'd love some details.

You could start by quickly browsing through the huge list of papers that cite Z3 [1].

Microsoft uses Z3 extensively for bug finding for all sort of products, notably through the SAGE tool. There is a great write up on its impact. [2]

From that paper:

"Finding all these bugs has saved millions of dollars to Microsoft, as well as to the world in time and energy, by avoiding expensive security patches to more than 1 billion PCs. The software running on your PC has been affected by SAGE. Since 2008, SAGE has been running 24/7 on an average of 100-plus machines/cores automatically fuzzing hundreds of applications in Microsoft security testing labs. This is more than 300 machine- years and the largest computational usage ever for any SMT (Satisfiability Modulo Theories) solver, with more than 1 billion constraints processed to date. SAGE is so effective at finding bugs that, for the first time, we faced “bug triage” issues with dynamic test generation."

[1] http://scholar.google.com/scholar?cites=4828743947843773221&...

[2] http://dl.acm.org/citation.cfm?id=2094081

Re: Z3: A high-performance theorem prover from Microsoft Research

#34

Post by tptacek »

psuter wrote: post #33
tptacek wrote: post #15

If people are using this for interesting projects, I'd love some details.

You could start by quickly browsing through the huge list of papers that cite Z3 [1]. Microsoft uses Z3 extensively for bug finding for all sort of products, notably through the SAGE tool. There is a great write up on its impact. [2] From that paper: "Finding all these bugs has saved millions of dollars to Microsoft, as well as to the world in time and energy, by avoiding expensive security patches to more than 1 bil…

I'm definitely familiar with Z3 and with solvers used offensively and defensively in software security. I'm just curious as to how widespread it's become with generalist software developers as a problem solving tool.

These are great links; thanks for posting them.

Re: Z3: A high-performance theorem prover from Microsoft Research

#35

Post by colanderman »

psuter wrote: post #31
colanderman wrote: post #17

Earlier quoted context omitted.

Last week I wrote a fun tool using it (actually, any SMT-LIB 2 compatible solver, of which Z3 seems to be the only open-source-ish one that works out of the box) to search for optimal branch-free load-free C implementations of small integer lookup tables (i.e. something the compiler should do but doesn't). It's really a minimal use of an SMT solver, but it saved me from having to think of a more clever algorithm than…

In case you or someone else is still looking, CVC4 [1] is a competitive open source alternative to Z3 or Yices. [1] http://cvc4.cs.nyu.edu/

Thanks! Last I checked (maybe a year back), something-or-other about CVC4 didn't work for me (I wholly forget what it was). I will try it out again.

I don't know if you are associated with CVC4 at all, but unfortunately the hashes of the amd64 Debian stable packages (cvc4, libcvc4-1, and libcvc4parser1) don't seem to match? It is probably just a package error however it makes me hesitant to install the packages…

Re: Z3: A high-performance theorem prover from Microsoft Research

#36

Post by tel »

tptacek wrote: post #34
psuter wrote: post #33

Earlier quoted context omitted.

You could start by quickly browsing through the huge list of papers that cite Z3 [1]. Microsoft uses Z3 extensively for bug finding for all sort of products, notably through the SAGE tool. There is a great write up on its impact. [2] From that paper: "Finding all these bugs has saved millions of dollars to Microsoft, as well as to the world in time and energy, by avoiding expensive security patches to more than 1 bil…

I'm definitely familiar with Z3 and with solvers used offensively and defensively in software security. I'm just curious as to how widespread it's become with generalist software developers as a problem solving tool. These are great links; thanks for posting them.

Do you have any links for using Z3 in security proofs?

Re: Z3: A high-performance theorem prover from Microsoft Research

#37

Post by lmeyerov »

tel wrote: post #32
shirkey wrote: post #30

What are the advantages/differences between this and Google's or-tools ( https://code.google.com/p/or-tools/ ), which is available under Apache license?

Without examining or-tools too much, I think it's solving a totally different problem. The Z3 guideis a good way to learn more ( http://rise4fun.com/z3/tutorial )

Z3 is about "satisfiability modulo theories", which basically means a SAT solver with smart extensions for things like floating point arithmetic that would otherwise die under a naive encoding. It's used for program verification, and in my group, program synthesis. OR tools like Google's choke on such problems that require reasoning about logic, recursive functions, etc.

For an example of a program verifier using Z3, Pex is amazing: pex4fun.com . It does 'whitebox' fuzzing (program analysis + SMT) to find inputs that break your assert statements and open-ended unit tests.

For an example of a program synthesizer, I spent the past few days writing a regular expression / sed script generator that infers the code from input/output pairs: http://lmeyerov.blogspot.com/2013/09/sneak-peek-for-my-stran... . Underneath, it calls into a SAT solver (it goes through Rosette[1], which plugs in its own solver or Z3).

[1] http://splashcon.org/2013/program/onward-research-papers/909...

Re: Z3: A high-performance theorem prover from Microsoft Research

#38

Post by psuter »

colanderman wrote: post #35
psuter wrote: post #31

Earlier quoted context omitted.

In case you or someone else is still looking, CVC4 [1] is a competitive open source alternative to Z3 or Yices. [1] http://cvc4.cs.nyu.edu/

Thanks! Last I checked (maybe a year back), something-or-other about CVC4 didn't work for me (I wholly forget what it was). I will try it out again. I don't know if you are associated with CVC4 at all, but unfortunately the hashes of the amd64 Debian stable packages (cvc4, libcvc4-1, and libcvc4parser1) don't seem to match? It is probably just a package error however it makes me hesitant to install the packages…

I am not associated with CVC4 directly (or Z3 for that matter). Something that is true for all these tools is that they evolve very quickly. As a result, you're better off building from source. In both cases, that means running `make` and nothing else.

Re: Z3: A high-performance theorem prover from Microsoft Research

#39

Post by apw »

microarchitect wrote: post #21

In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving. If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394 . To make a long story short, various problems in program verification and static analysis have seen success with…

Is STP considered a qualitatively different kind of tool than Yices and Z3?

Re: Z3: A high-performance theorem prover from Microsoft Research

#40

Post by beambot »

microarchitect wrote: post #21

In terms of applicability, SMT (satisfiability module theory) solvers basically allow you to do things which are slightly more complex than plain SAT solving. If you're looking to learn more, Leonardo has a nice introduction to SMT and its applications over here: http://dl.acm.org/citation.cfm?id=1995394 . To make a long story short, various problems in program verification and static analysis have seen success with…

Pardon the relative ignorance... but I thought these types of problems (SAT and SMT) were NP-Complete in the general case? Does Z3 do something special (eg apply heuristics)? It looks very impressive!
Post reply on HN