Relational Analysis of Non-deterministic Integer Programs
Event details
| Date | 20.06.2011 |
| Hour | 14:15 |
| Speaker | Dr Radu Iosif, Véermag, CNRS and University of Grenoble |
| Location | |
| Category | Conferences - Seminars |
Automatic inference of function summaries is the key to compositional verification of numerical programs. In the first part of this talk I will present an algorithm for verifying hierarchical non-recursive programs, based on an efficient computation of transitive closures for several classes of program loops: difference bounds, octagonal and
finite monoid affine relations.
On the theoretical side, this provides a common solution to the acceleration problem, for all these three classes of relations. In practice, according to our experiments, the new method performs up to four orders of magnitude better than the previous ones for the first two classes.
In the second part of the talk, I explain how transitive closure computation combines with other methods (quantifier elimination, abstraction, etc.) in order to provide a framework for the analysis of such systems. These ideas led us to the implementation of the FLATA tool.
Joint work with Marius Bozga and Filip Konecny.
Prof. Iosif's homepage
Practical information
- General public
- Free