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 based on (1) computing
over-approximations A1 and A2 of L1 and L2, (2) checking if the
intersection of A1 and A2 is non-empty, and, if the non-empty
intersection represents an infeasible trace, (3) refining these
over-approximations A1 and A2. Furthermore, we present new fully
automatic predicateabstraction refinement techniques to obtain
communicating pushdown systems from C source code. We have implemented
our techniques in the model-checker MAGIC. We report our experimental
results on some non-trivial benchmarks.
(Click here to access the paper:
PostScript,
PDF.)