Incremental SMT-based model checking of synchronous systems

Опубликовано 28 июля 2016, 0:22

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.