Invited  Talk

Context Bounded Model Checking of Concurrent Software

Shaz Qadeer (Microsoft Research, USA)

Designing concurrent programs is difficult. The nondeterministic interaction between concurrently executing threads of a concurrent program results in programming errors that are notoriously difficult to reproduce and fix. Automated program analysis techniques for finding such errors are invaluable as a debugging and programming aid. In this talk, I will present a novel static analysis technique for concurrent software based on the idea of context-bounded model checking. An execution of a concurrent program is a sequence of contexts, where each context is an uninterrupted sequence of transitions performed by a single thread. Our work is motivated by our observation that many subtle errors in a concurrent program are manifested by executions with few contexts. I will first present KISS (Keep It Simple and Sequential), a technique for transforming a concurrent program P into a sequential program Q that encodes all executions of P with a small number of contexts. We used KISS to convert SDV (Static Driver Verifier), a model checker for sequential C programs, into a model checker for concurrent C programs. The combination of KISS and SDV has found a variety of subtle concurrency errors in Windows device drivers. Next, I will present a new theoretical result which shows that bounding the number of contexts significantly reduces the complexity of verifying concurrent programs. It is well-known that the problem of verifying assertions in a concurrent boolean program is undecidable. I will show that if analysis is limited to executions with a fixed but arbitrary context-bound, the problem becomes decidable, even in the presence of unbounded dynamic thread creation.

Back to technical programme page