Taking Satisfiability to the Next Level with Z3

Date: Wednesday, May 30, 2012
Speaker: Nikolaj Bjorner
Venue: TU Vienna
Notes:

Fritz Paschke HS, Gusshaustrasse

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.

Posted in RiSE Seminar