Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach

A fully automated compositional framework which combines two orthogonal abstraction techniques within a counterexample-guided abstraction refinement (CEGAR) scheme which incrementally increases the granularity of the abstractions until the specification is either established or refuted.

Abstract

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 (CEGAR) 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. To our knowledge, this is the first compositional use of CEGAR in the context of model checking concurrent C programs. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC.