LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs
- Date
- Tuesday, November 08 2011 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Peter Schrammel (INRIA Rhône-Alpes, Grenoble, France)
We are interested in the verification of safety properties about synchronous data-flow programs with Boolean and numerical variables, e.g., Lustre programs. We rely on reachable-state analysis for this problem. Two main techniques for ensuring the termination of such an analysis are acceleration and widening (within the abstract interpretation framework).
Acceleration-based methods lead to exact results, but they guarantee termination only for a restricted class of programs. Widening is less precise and less predictable but does not have this limitation. Abstract acceleration integrates acceleration techniques into the abstract interpretation framework, such as to reduce the need for widening and thus to improve precision.
All these techniques however require the enumeration of the Boolean state-space, which leads to a state-space explosion even for medium-sized Lustre programs. In this talk we propose a solution by extending numerical acceleration to logico-numerical acceleration. We define logico-numerical abstract acceleration methods based on a partial decoupling of Boolean and numerical transitions and we show how well-chosen partitioning techniques make them effective. Experimental results show that incorporating these methods in a verification tool based on abstract interpretation provides not only significant advantage in terms of precision, but also a gain in performance.