Verifying Concurrent Message-Passing C Programs with Recursive Calls
S. Chaki, E. Clarke, N. Kidd, T. Reps, and T. Touili
We consider the model-checking problem for C programs with (1) data
ranging over very large domains, (2) (recursive) procedure calls, and
(3) concurrent parallel components that communicate via synchronizing
actions. We model such programs using communicating pushdown
systems, and reduce the reachability problem for this model to
deciding the emptiness of the intersection of two context-free
languages L1 and L2. We tackle this undecidable
problem using a CounterExample Guided Abstraction Refinement (CEGAR)
scheme. We implemented our technique in the model checker MAGIC and
found a previously unknown bug in a version of a Windows NT Bluetooth
driver.
(Click here to access the paper:
PostScript,
PDF,
(c) Springer-Verlag.)