Taking Satisfiability to the Next Level with Z3

This RiSE Seminar Talk was held by Nikolaj Bjorner on May 30th, 2012.

ABSTRACT

Several applications from program analysis, design and testing rely critically on solving SMT problems. Many applications build on top of SMT solvers in sophisticated ways by carefully crafting the solver interaction. Many applications at their core solve for recursive predicates and so far SMT solvers have no direct support for these. This talk presents a new extension of Z3 and an algorithm, PDR extended to SMT domains, for handling recursive predicates. The IC3 algorithm was recently introduced for proving properties of finite state reactive systems. It has been applied very successfully to hardware model checking.

We provide a specification of the algorithm using an abstract transition system and highlight its dual operation: model search and conflict resolution. We then generalize it along two dimensions. Along one dimension we address nonlinear fixed-point operators (push-down systems) and evaluate the algorithm on Boolean programs. In the second dimension we leverage proofs and models and generalize the method to Boolean constraints involving theories. A side-effect of our approach is a model-based method for computing interpolants of recursion-free Horn clauses for linear real arithmetic. The method also produces a decision procedure for timed push-down systems.

The talk is based on joint work with Krystof Hoder that will appear at SAT 2012.

Note: This lecture is part of the RiSE Seminar (http://www.arise.or.at/?id=seminar), and is organised by the Austrian Society for Rigorous Systems Engineering.

BIO:

Nikolaj Bjorner is a senior researcher in the Research in Software Engineering group at Microsoft Research, Redmond. His main line of work is around the state-of-the-art SMT constraint solver Z3 with Leonardo de Moura. Z3 is used for program verification and test case generation. In his previous lives he wrote STeP, the Stanford Temporal Prover, and he was in the Core File Systems group where he designed and implemented the core of the distributed file replication system, DFS-R, and the content dependent chunking algorithms in the remote differential compression protocol RDC.