Verification of parameterized concurrent programs

Date: Thursday, May 12, 2011
Speaker: Azadeh Farzan
Venue: TU Vienna
Notes:

188/2 – @ 17.00

In this talk, we discuss the verification problem of parameterized concurrent programs. We propose a semi-compositional reasoning method for verifying safety properties of infinite-thread programs based on computing an over-approximation of the set of reachable states. Our approach is sound and terminating, even for infinite state programs (e.g. programs with recursion or unbounded integers). The essential idea of the technique is to reason about a program with many threads by considering only two thread abstractions at a time, and then combining information across all pairs of threads. Our algorithm consists of a feedback loop that combines techniques from abstract interpretation to compute numerical invariants with techniques from model checking to compute the effects of interference. We implemented our approach in a prototype tool and evaluated it on a selection of parameterized programs including Boolean programs generated by the SatAbs tool by performing predicate abstraction on Linux device drivers.

Posted in RiSE Seminar