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. © 2011 Springer-Verlag.
CITATION STYLE
Kahsai, T., Ge, Y., & Tinelli, C. (2011). Instantiation-based invariant discovery. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6617 LNCS, pp. 192–206). https://doi.org/10.1007/978-3-642-20398-5_15
Mendeley helps you to discover research relevant for your work.