Seminar by Ashutosh Gupta
Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs
Ashutosh Gupta
IST Austria.
Date: Monday, December 12th, 2011
Time: 11AM
Venue: CS102.Abstract:
Automated verification of multi-threaded programs requires explicit identification of the interplay between interacting threads, so called environment transitions, to enable scalable, compositional reasoning. Once the environment transitions are identified, we can prove program properties by considering each program thread in isolation, as the environment transitions keep track of the interleaving with other threads. Finding adequate environment transitions that are sufficiently precise to yield conclusive results and yet do not overwhelm the verifier with unnecessary details about the interleaving with other threads is a major challenge.
In this work, we proposed a method for safety verification of multi-threaded programs that applies (transition) predicate abstraction-based discovery of environment transitions, exposing a minimal amount of information about the thread interleaving. The crux of our method is an abstraction refinement procedure that uses recursion-free Horn clauses to declaratively state abstraction refinement queries. Then, the queries are resolved by a corresponding constraint solving algorithm. We present preliminary experimental results for mutual exclusion protocols and multi-threaded device drivers.