Instantiation-based invariant discovery

Abstract. We present a general scheme for automated instantiation-based in-variant discovery. Given a transition system, the scheme produces k-inductive in-variants from templates representing decidable predicates over the system’s data types. The proposed scheme relies on efficient reasoning engines such as SAT and SMT solvers, and capitalizes on their ability to quickly generate counter-models of non-invariant conjectures. We discuss in detail two practical specializations of the general scheme in which templates represent partial orders. Our experimen-tal results show that both specializations are able to quickly produce invariants from a variety of synchronous systems which prove quite useful in proving safety properties for these systems.