Automatic Theorem Proving and SMT

Presented as part of the 2013 HCSS conference.

ABSTRACT

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.