Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Laurent Doyen and Stefan Göller.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Logico-Numerical Abstract Acceleration and Application to the Verification of Data-Flow Programs

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Peter Schrammel
Date
Le mardi 08 novembre 2011 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
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.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

No entries.

Les séminaires précédents