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

From Counter Abstraction to Thread-State Cutoffs: New Techniques for Multi-Threaded Program Verification

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

 Thomas Wahl
Le mardi 20 avril 2010 à 11:00
Salle de Conférence (Pavillon des Jardins)
Thomas Wahl (Oxford University)

The formal analysis of multi-threaded programs is among the grand challenges of software verification research. In this talk, I describe our recent and ongoing work on analyzing parameterized finite-state programs, such as non-recursive multi-threaded Boolean programs, a principal ingredient in predicate abstraction. I begin with a scalable method for analyzing the reachability of program locations in programs executed by a bounded number of threads. This method, being based on counter abstraction, extends in principle to unbounded thread counts, but suffers in practice from the high complexity of coverability and reachability analyses for certain types of counter machines. A different approach to program location reachability rests on the assumption that in practical parametric program settings, a small "cutoff" number of threads suffice to generate all reachable program locations. While this assumption is widely considered to be safe, its practical usefulness hinges on how accurately we are able to estimate the cutoff of a given program. I present a new method that analyses the reachable state space of a replicated finite-state program for increasing thread counts, until a condition emerges that allows us to conclude that the cutoff thread count has been reached. Completeness of this method is achieved by resorting to traditional coverability analyses in corner cases. The result is a precise and efficient program location reachability method for replicated finite-state programs run by arbitrarily many threads.

À 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