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
From Counter Abstraction to Thread-State Cutoffs: New Techniques for Multi-Threaded Program Verification
- Date
- Tuesday, April 20 2010 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.