The state space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (operating respectively on data and events) within a counterexample-guided abstraction refinement scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Our explicit use of compositionality delays the onset of state space explosion for as long as possible. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC.
Proceedings of SoftMC 03, ENTCS 89(3), 2003. 16 pages.
PostScript / PDF
© 2003 Elsevier Science B.V.