×

Automated compositional abstraction refinement for concurrent C programs: a two-level approach. (English) Zbl 1271.68081

Dawar, Anuj (ed.), SoftMC 2003. Workshop on software model checking (satellite workshop of CAV ’03), Ottawa, Canada, June 26–27, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 89, No. 3, 417-432 (2003).
Summary: 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.
For the entire collection see [Zbl 1271.68030].

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Bandera; MAGIC
PDFBibTeX XMLCite
Full Text: Link