Unleashing the Verification Genie in the Cloud

Z3 is a state-of-the-art SMT (Satisfiability Modulo Theories) solver available from Microsoft Research. It is used as a logic engine in several program analysis, test-generation and verification systems. Z3 exposes a number of APIs for these applications, but is in itself a low-level tool. We discuss the design trade-offs we have faced and different ways we lower the barrier of entry to use Z3. This includes using programming language abstractions, such as quotations and LINQ (Language Integrated Query features) and exposing Z3 as a web service.