Instantiation-Based Invariant Discovery

Temesghen Kahsai; Yeting Ge; Cesare Tinelli

doi:10.1007/978-3-642-20398-5_15

Back

Book chapter

Peer reviewed

Instantiation-Based Invariant Discovery

Temesghen Kahsai, Yeting Ge and Cesare Tinelli

NASA Formal Methods, pp.192-206

Lecture Notes in Computer Science, Springer Berlin Heidelberg

2011

DOI: 10.1007/978-3-642-20398-5_15

View Online

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.

Invariant Generation

Model Check

Partial Order

Predicate Abstraction

Safety Property

Details

Title: Subtitle: Instantiation-Based Invariant Discovery
Creators: Temesghen Kahsai - University of Iowa
Yeting Ge - University of Iowa
Cesare Tinelli - University of Iowa
Resource Type: Book chapter
Publication Details: NASA Formal Methods, pp.192-206
Publisher: Springer Berlin Heidelberg; Berlin, Heidelberg
Series: Lecture Notes in Computer Science
DOI: 10.1007/978-3-642-20398-5_15
eISSN: 1611-3349
ISSN: 0302-9743
Language: English
Date published: 2011
Academic Unit: Computer Science
Record Identifier: 9984259473202771

Metrics

7 Record Views