salle A. Turing CE4
14 avril 2014 - 15h00
Incremental Invariant Generation using Logic-based Automatic Abstract Transformers
par Cesare Tinelli de University of Iowa
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 present a completely automatic method for building abstract interpreters which, in addition, can generate sound invariants 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.
This is joint work with Pierre-Loïc Garoche and Temesghen Kahsai
