BT

Facilitating the Spread of Knowledge and Innovation in Professional Software Development

Write for InfoQ

Topics

Choose your language

InfoQ Homepage News LINQ to Z3, The World’s Fasted Theorem Prover

LINQ to Z3, The World’s Fasted Theorem Prover

Leia em Português

Microsoft Research claims that Z3 is the world’s fastest theorem prover. Z3 is designed to be a low-level tool for other applications, it is not meant to stand-alone. With its host of theorem provers, it is used by numerous projects including Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC.

Using Z3’s .NET API, one can encode theorems using an object-orientated style. However the example in the Z3 Tutorial demonstrates that even small problems can be quite tedious to code. Bart De Smet greatly simplified this by wrapping the OO-style API with a query-style API called LINQ to Z3. Below is an example that accompanied Bart De Smet’s Channel 9 interview.

  var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
    where t.X1 - t.X2 >= 1
    where t.X1 - t.X2 <= 3
    where t.X1 == (2 * t.X3) + t.X5
    where t.X3 == t.X5
    where t.X2 == 6 * t.X4
    select t; 
  var solution = theorem.Solve();
  Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}",

Support for Z3 primarily available on Windows, but there is a Linux version of Z3. Z3 is released for non-commercial use under the “Microsoft Research License Agreement”. You can play with an on-line version of Z3 on RiSE4fun.

Rate this Article

Adoption
Style

BT