Book chapter
Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers
NASA Formal Methods, pp.139-154
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2013
DOI: 10.1007/978-3-642-38088-4_10
Abstract
Formal analysis tools for system models often require or benefit from the availability of auxiliary system invariants. Abstract interpretation is currently one of the best approaches for discovering useful invariants, in particular numerical ones. However, its application is limited by two orthogonal issues: (i) developing an abstract interpretation is often non-trivial; each transfer function of the system has to be represented at the abstract level, depending on the abstract domain used; (ii) with precise but costly abstract domains, the information computed by the abstract interpreter can be used only once a post fix point has been reached; this may take a long time for large systems or when widening is delayed to improve precision. We propose a new, completely automatic, method to build abstract interpreters which, in addition, can provide sound invariants of the system under analysis before reaching the end of the post fix point computation. In effect, such interpreters act as on-the-fly invariant generators and can be used by other tools such as logic-based model checkers. We present some experimental results that provide initial evidence of the practical usefulness of our method.
Details
- Title: Subtitle
- Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers
- Creators
- Pierre-Loïc Garoche - University of IowaTemesghen Kahsai - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- NASA Formal Methods, pp.139-154
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-38088-4_10
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2013
- Academic Unit
- Computer Science
- Record Identifier
- 9984259473602771
Metrics
15 Record Views