Instantiation-Based Invariant Discovery

10 years 12 months ago
Instantiation-Based Invariant Discovery
Abstract. We present a general scheme for automated instantiation-based invariant discovery. Given a transition system, the scheme produces k-inductive invariants 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 experimental 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.
Temesghen Kahsai, Yeting Ge, Cesare Tinelli
Added 29 May 2011
Updated 29 May 2011
Type Journal
Year 2011
Where NFM
Authors Temesghen Kahsai, Yeting Ge, Cesare Tinelli
Comments (0)