Verification of large multithreaded programs is challenging.

Automatic approaches cannot overcome the state explosion in the number

of threads; semi-automatic methods require expensive human time

for finding global inductive invariants. Ideally, automatic methods should

not deal with the composition of the original threads and a human should

not supply a global invariant. We provide such an approach. In our approach,

a human supplies a specification of each thread in the program.

Here he has the freedom to ignore or to use the knowledge about the

other threads. The checks whether specifications of threads are sound

as well as whether the composition of the specifications is error-free are

handed over to the off-the-shelf verifiers. We show how to apply this

divide-and-conquer approach for the interleaving semantics with shared

variables communication where specifications are targeted to real-world

programmers: a specification of a thread is simply another thread. The

new approach extends thread-modular reasoning by relaxing the structure

of the transition relation of a specification. We demonstrate the

feasibility of our approach by verifying two protocols governing the teardown

of important data structures in Windows device drivers.

In  Conference on Verification, Model Checking, and Abstract Interpretation

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details