Invariant stream generators using automatic abstract transformers based on a decidable logic
This addresses the problem of non-trivial development and slow invariant computation in formal analysis for researchers and practitioners in program verification, though it appears incremental as it builds on existing abstract interpretation techniques.
The paper tackles the difficulty of developing abstract interpreters for invariant generation by proposing an automatic method that builds interpreters capable of providing sound invariants before completing post fix point computations, enabling on-the-fly invariant generation.
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.