Copenhagen Programming Language Seminar

SMT solvers for Testing, Program Analysis and Verification at Microsoft

Nikolaj Bjørner
Microsoft Research Redmond, USA

Monday, June 22, 2009, 15:00-16:00
DTU Informatics, Bldg. 305, Room 053


Decision procedures for checking satisfiability of logical formulas are crucial for many testing, program analysis and verification applications. Of particular recent interest are solvers for Satisfiability Modulo Theories (SMT). SMT solvers are theorem provers that allow combining specialized algorithms for checking satisfiability from different domains. We will describe how SMT solvers, and the state-of-the art solver Z3 in particular, are used in program analysis and verification.

I will present several applications from program analysis at Microsoft. These applications include dynamic-symbolic test-case generation tools Pex and SAGE, SAGE, in particular, has been recently very successful on identifying and preventing security vulnerabilities in Microsoft code; they include the static analysis tools HAVOC and the well-established tool PREfix which is used on most Microsoft code bases prior to shipping; and they include the program verification tools Spec#/Boogie and the C verification system, VCC, currently used for detailed verification of the Viridian Hypervisor. I will describe the key techniques that were used for bridging the program test/analysis and verification domains into the SMT solver and some of the theory that was crucial for building an industrial-strength solver.

The SMT solver Z3 is available freely for academic use from http://research.microsoft.com/projects/z3. It has been currently been integrated with several Microsoft program analysis, test and verification tools, including Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, SAGE, VCC, PREfix, VS3, M3, FORMULA, and HAVOC. It is also used by several external users. Z3 participated in the SMT-COMP'08 competition associated with CAV. Z3 did very well, it took 9 first places and 6 second places. It also participated in the SMT-COMP'07 competition associated with CAV, where it took 4 first places and 7 second places.

Bio: I am managing the Foundations of Software Engineering (FSE) group at Microsoft Research in Redmond. FSE's current research projects span logics for authentication (Yuri Gurevich, DKAL), model programs (Margus Veanes, M3), parameterized unit test case generation (Nikolai Tillmann and Peli de Halleux, Pex), and model-based techniques for constructing domain specific languages (Ethan Jackson, BAM/FORMULA). My current main work is around the SMT solver Z3 jointly with Leonardo de Moura. A curious fact: it is about 20 years since I started university at DTU and with stints at DIKU.

Scientific host:Michael R. Hansen Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org