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 Stéphane Le Roux and Matthias Fuegger.

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

Séminaires passés

Constrained Environment Assumptions for Multi-Threaded Programs

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

Date
Le mardi 30 mars 2010 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Andrey Rybalchenko (TU München)

Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so-called environment assumptions, to enable scalable reasoning. Once identified, these assumptions can be used for reasoning with one program thread at a time, which is possible by using the respective environment assumption to model the interleaving with other threads. Finding adequate assumptions that are sufficiently precise to yield conclusive results and yet keep track only of necessary facts about the execution environment in order to scale well is a major challenge. In this talk I will present a constraint-based technique for the inference of such assumptions. Our technique automatically steers towards an optimal precision/efficiency trade-off between the extremes of efficient, but incomplete thread-modular reasoning and complete, but prohibitively expensive consideration of all interleavings. For this task, we pinpoint a declarative formulation of modular verification that allows one to express requisite environment assumptions using constraints and admits algorithmic solutions based on abstract fixpoint checking. I will describe an application of our environment assumption inference for the verification of reachability and termination properties of multi-threaded programs. Joint work with Ashutosh Gupta and Corneliu Popeea


À propos du LSV

Agenda des séminaires

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

mar. 19 février

Les séminaires précédents