Preprint
Invariant stream generators using automatic abstract transformers based on a decidable logic
ArXiv.org
05/16/2012
DOI: 10.48550/arxiv.1205.3758
Abstract
The use of formal analysis tools on models or source code often requires the
availability of auxiliary invariants about the studied system. Abstract
interpretation is currently one of the best approaches to discover useful
invariants, especially 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; something that may
take a long time for very large system analysis or with delayed widening to
improve precision.
This paper proposes a new, completely automatic, method to build abstract
interpreters. One of its nice features is that its produced interpreters can
provide sound invariants of the analyzed system before reaching the end of the
post fix point computation, and so act as on-the-fly invariant generators.
Details
- Title: Subtitle
- Invariant stream generators using automatic abstract transformers based on a decidable logic
- Creators
- Pierre-Loïc GarocheTemesghen KahsaiCesare Tinelli
- Resource Type
- Preprint
- Publication Details
- ArXiv.org
- DOI
- 10.48550/arxiv.1205.3758
- ISSN
- 2331-8422
- Language
- English
- Date posted
- 05/16/2012
- Academic Unit
- Computer Science
- Record Identifier
- 9984411061402771
Metrics
2 Record Views