Incremental SMT-based model checking of synchronous systems

This talk provides an overview of our current research on SMT-based model checking.
We present an incremental and parallel model checking architecture to verify safety properties of synchronous systems. The architecture, implemented in the Lustre model checker Kind, relies on SMT solvers as its main inference engines. It is designed to minimize synchronization delays between subprocesses and accommodate the incorporation of automatic auxiliary invariant generators to enhance the main verification algorithm (k-induction). It also allows the verification of multiple properties incrementally and the use of proven input properties to aid the verification of the remaining ones.
We also present a general scheme for instantiation-based invariant discovery that can be used to implement invariant generators for the architecture above.
The scheme generates k-inductive invariants for a given transition system from any template R[_,_] representing a decidable predicate over one of system’s data types. The scheme itself relies on efficient SMT solvers, and capitalizes on their ability to quickly generate counter-models of non-invariant conjectures.
We discuss two specializations of the general scheme that make it feasible in practice. Finally, we provide some experimental evidence showing how parallelism, incrementally and invariant generation improve the speed and the precision of the baseline k-induction algorithm.

Speaker Details

Cesare Tinelli is an associate professor of Computer Science and Collegiate Scholar at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His research interests include automated reasoning, formal methods, software verification, and applications of logic in computer science. His research has been funded by the US National Science Foundation, the Air Force Office of Scientific Research, and Intel Corp., and has appeared in more than
40 refereed publications. He has given invited talks at such conferences as CAV, HVC, NFM, TABLEAUX, VERIFY, and WoLLIC.
He is a founder and leader of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for Satisfiability Modulo Theories solvers.
He was a co-recipient of the Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community, and of an NSF CAREER award in 2003. He has served in the program committee of numerous automated reasoning conferences and workshops, and in the steering committee of CADE, IJCAR, FTP, FroCoS and SMT. He was the PC chair of FroCoS’11 and has been an associate editor of the Journal of Automated Reasoning since 2007.