Seminars

Kind-AI: When abstract interpretation and SMT-based model-checking meets (PDF)

Pierre-Loic Garoche - Visiting Assistant Professor at University of Iowa On leave from ONERA-French Aerospace Laboratory

04/13/2012, 2pm, GHC-4405

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 talk presents 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.

Biography

Pierre-Loïc Garoche is a research scientist at Onera, the French Aerospace Lab. He graduated from École Normale Supérieure de Cachan, France, and received his PhD degree in Computer Science from the University of Toulouse, France in 2008. He was then addressing the static analysis of concurrency using abstract interpretation. At Onera, his work is mainly focused on the use of formal methods in critical embedded systems development, in a certified context. His primary interest is at the frontier between academic research and industry, combining analyses to achieve software verification and validation. He is participating with numerous research projects and industrial partnerships on these topics at both national and international levels.

He is currently on a sabbatical leave at the University of Iowa.