Program Analysis and Testing using Efficient Satisfiability Modulo Theories Solving

This talk describes the Satisfiability Modulo Theories (SMT) solver, Z3, from Microsoft Research. Z3 is a state-of-the art theorem prover that integrates specialized solvers for domains that are of relevance for program analysis, testing and verification. Z3 is a compelling integral component of such tools because these tools rely on reasoning about program states and transformations between states in ways that are slightly disguised as SMT problems.

We describe uses of Z3, including the Windows 7 static driver verifier, the SAGE white-box fuzzer for finding security vulnerabilities, a cloud service security policy checker, the Pex test-case generation tool, a verifying C compiler and JavaScript malware detection, among others. We also give some background on the foundations and technologies used in modern high-performance theorem provers.