Cesare Tinelli's Publications

Temesghen Kahsai, Yeting Ge, and Cesare Tinelli. Instantiation-Based Invariant Discovery. In Proceedings of the 3rd NASA Formal Methods Symposium, Pasadena, CA, 2011. ©Springer

Abstract. We present a general scheme for automated instantiation-based invariant 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 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.