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

Add to your list(s) Download to your calendar using vCal

• Thomas Wahl
• Tuesday 27 April 2010, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

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 non-recursive concurrent Boolean programs run by arbitrarily many threads.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.