Programming Constraint Services with Z3

by Nikolaj Bjorner

Abstract
Many program verification, analysis, testing and synthesis queries reduce to solving satisfiability of logical formulas. Yet, there are several applications where satisfiability, and optionally a model or a proof, is insufficient. Examples of useful additional information include interpolants, models that satisfy optimality criteria, generating strategies for solving quantified formulas, enumerating and counting solutions. We will cover some of the newer features in Z3 that expose constraint services. For applications in product configuration, Z3 includes specialized solvers for finding backbones under assumptions, for solving quantified formulas Z3 contains elements of partial quantifier elimination methods based on models, and for solving optimization modulo SMT, Z3 contains dedicated MaxSMT.

Bio
Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work with Leonardo de Moura  and Christoph Wintersteiger is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 received the 2015 ACM SIGPLAN Software System award and most influential tool paper in the first 20 years of TACAS in 2014. Previously, he developed the DFSR, Distributed File System - Replication, and Remote Differential Compression protocols, RDC, part of Windows Server since 2005 and before that worked on distributed file sharing systems at a startup, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first few years of university at DTU and DIKU.

More information