Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs

Date: Thursday, February 03, 2011
Speaker: Ashutosh Gupta
Venue: IST Austria

Starts at 15:00

Automated verification of multi-threaded programs requiresexplicit identification of the interplay betweeninteracting threads, so called environment transitions, toenable scalable, compositional reasoning. Once theenvironment transitions are identified, we can proveprogram properties by considering each program thread inisolation, as the environment transitions keep track ofthe interleaving with other threads. Finding adequateenvironment transitions that are sufficiently precise toyield conclusive results and yet do not overwhelm theverifier with unnecessary details about the interleavingwith other threads is a major challenge.

In this talk, I will present a method for safetyverification of multi-threaded programs that applies(transition) predicate abstraction-based discovery ofenvironment transitions, exposing a minimal amount ofinformation about the thread interleaving. The crux of ourmethod is an abstraction refinement procedure that usesrecursion-free Horn clauses to declaratively stateabstraction refinement queries. Then, the queries areresolved by a corresponding constraint solvingalgorithm. We present preliminary experimental results formutual exclusion protocols and multi-threaded devicedrivers.

Posted in RiSE Seminar