BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From Counter Abstraction to Thread-State Cutoffs:\nNew Techniques 
 for Multi-Threaded Program Verification - Thomas Wahl
DTSTART:20100427T120000Z
DTEND:20100427T130000Z
UID:TALK23469@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:The formal analysis of multi-threaded programs is among the gr
 and challenges of software verification research. In this talk\, I describ
 e our recent and ongoing work on analyzing parameterized finite-state prog
 rams\, such as non-recursive multi-threaded Boolean programs\, a principal
  ingredient in predicate abstraction. I begin with a scalable method for a
 nalyzing the reachability of program locations in programs \nexecuted by a
  bounded number of threads. This method\, being based on counter abstracti
 on\, extends in principle to unbounded thread counts\, but suffers in prac
 tice from the high complexity of coverability and reachability analyses fo
 r certain types of counter machines. A different approach to program locat
 ion reachability rests on the assumption that in practical parametric prog
 ram 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 \nhinges on how accurately we are able
  to estimate the cutoff of a given program. I present a new method that an
 alyses the reachable state space of a replicated finite-state program for 
 increasing thread counts\, until a condition emerges that allows us to con
 clude that the cutoff thread \ncount has been reached. Completeness of thi
 s method is achieved by resorting to traditional coverability analyses in 
 corner cases. The result is a precise and efficient program location reach
 ability method for non-recursive concurrent Boolean programs run by arbitr
 arily many \nthreads.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR