Keynote

nZ – Objective Functions in Z3

Nikolaj Bjorner, Microsoft Research

Satisfiability Modulo Theories, SMT, solvers are used in many applications that benefit from the power of newer theorem proving technologies and logical expressiveness of supported logics and specialized theory solvers. Applications use SMT solvers to determine whether formulas are satisfiable, and in the case they are often need as feedback models that are given as assignments to free variables. Yet in many cases arbitrary assignments are insufficient and applications are really solving optimization problems: one or more values should be minimal or maximal with respect to a Pareto front or a lexicographic priority. So far, users of Z3, an SMT solver from Microsoft Research, build custom loops to achieve objective values. In this talk I introduce nZ (new-Z, or max-Z), an extension within Z3 that lets users formulate objective functions directly with Z3. Under the hood is a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations.

nZ was initiated with Anh-Phan Dung who was at Microsoft Research for an internship.

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 is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 is developed by Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger. Previously, he designed the DFSR, Distributed File System - Replication, shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, 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 three years of university at DTU and DIKU.