Visible to the public Automatic Theorem Proving and SMT


Automated reasoning has become an integral part of software engineering tools in recent years thanks to high-performance theorem provers. The Satisfiability Modulo Theories (SMT) solver Z3 from Microsoft Research powers a generation of tools, including SAGE, Pex, Spec#, Dafny, VCC, Havoc, Boogie, Slam, Yogi, Spec Explorer, SecGuru, and Terminator. These tools reduce program analysis, verification and testing problems to logic queries that are solved using Z3. The talk takes these applications of Z3 as a starting point. The application SecGuru is examined in more depth. It is a tool for automatically validating network connectivity restriction policies in large scale data-centers such as Azure. We then describe some of the current trends in Z3: including solving recursive Horn clauses, solving real and floating point arithmetic.

Creative Commons 2.5

Other available formats:

Automatic Theorem Proving and SMT