[ot]

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.

[1] http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories

[2] http://rise4fun.com/Z3/bit-count

[3] http://rise4fun.com/Z3Py/nonlinear

[olliesaunders]

It seems its only free for non-commercial use, ergo not free.

[ot]

You are absolutely right. I was excited because I can finally read the code and learn something from it.

But of course the implication "open source -> I can use it anywhere I want" is broken in this case. The author should have been a little more careful in not abusing that term, even if this was posted on his blog.

I am well aware of that licence, I myself had to use it for some code I wrote while at MSR [1]. I was not happy at all about the non-commercial clause, but it was either that or not releasing the code. I guess the same happened here.

[1] https://github.com/ot/path_decomposed_tries/blob/master/LICE...

[pascal_cuoq]

> 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:

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]

what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.

[tptacek]

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.

[krenoten]

Things like automatic exploit generation[1] and exploit hardening[2] in particular rely on SMT solvers to accomplish their goals. They allow for some truly remarkable things to be done. Expect skynet to utilize them heavily in its distributed automatic exploit generation (global autopwn) tooling!

1. http://security.ece.cmu.edu/aeg/ 2. http://users.ece.cmu.edu/~ejschwar/bib/schwartz_2011_rop-abs...

[ufo]

Are you familiar on how you can use SAT solvers to solve a wide variety of constraint problems?

https://github.com/hugomg/hexiom

SMT solvers basically extend SAT solvers to allow you to work directly with other theories (linear inequalities, bit arrays, etc) without being forced to encode this as the booloean formulas that basic SAT understand. The idea is that dealing with the higher level details directly instead of having to convert tihngs to a commo low level makes it simpler to express things and can also allow for custumized optimizations and algorithms?

[Dn_Ab]

I have only made light contact with SMTs in my explorations but SMT solvers have massive applicability. They're used in theorem proving - verification, dependent typing, contracts - scheduling, planning, and for understanding/modelling cell regulatory networks in biology.

Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (just as linear programming shows just cause something is in P doesn't mean it is 'easy' - for large values of easy). To ground the concept you can roughly categorize it with logic programming, answer set programming, constraint satisfaction and integer programming. I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.

[mjn]

> I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.

I suppose it depends on what you mean by flexible. I would say that ASP is more flexible as a modeling language—you can specify all sorts of logic and constraints in it in a fairly expressive logical formalism, with both generative (Prolog-like) and constraint-oriented (CSP-like) language constructs. Particularly with the extensions the Potassco people have been making in their version: http://potassco.sourceforge.net/

However, current ASP solvers ground to variable-free (propositional) programs before solving, which means they blow up on large-ish integer domains, since you end up propositionalizing the whole integer range. I've had some examples where just grounding out the problem takes ages, but then it's nearly instant to solve once the grounding is done. SMT avoids that by providing a way to ground "modulo" a domain theory, rather than fully grounding, with a theory of integers being a common example.

[Dn_Ab]

Awesome response thanks. The increased ease of use for modeling is part of why I decided on it rather than an SMT solver. One should prefer ASP wherever the assumptions hold. I use(d) DLV-Complex but will check your link.

But right, by more flexible I meant the availability of quantifiers in SMT solvers.

[tikhonj]

They can be used for program synthesis. That is, given some high-level specification, you can use an SMT solver to generate code fitting that specification. You can also use them to verify that some code does fit a specification and, if it doesn't, to find the part of the code causing the actual problem (the minimal unsat core).

A particular example would be to take some existing code with holes (just parts left out) and some assertions about the code's behavior, encode both as logic formulas and try to find a satisfying assignment for the holes. When you have a possible assignment, you can verify it with the same encoding. You can then use the satisfying assignment to fill in the holes in the initial program, which are ideally very tedious to code by hand.

[agravier]

Planning problems can be encoded as SAT problems, for instance.

[raphinou]

another example: package dependencies resolution on Linux distributions.

[wolfgke]

This can far more easily be done by topological sorting.

[gchpaco]

That's not actually sufficient when you consider version requirements; for example requiring a specific range of libc or the like.

[ac]

Various forms of program analysis/verification. Some examples of applications where SMT is heavily used are automated theorem provers, symbolic execution engines, model checking tools.