There has been considerable progress in the domain of software
verification over the last few years. This advancement has been
driven, to a large extent, by the emergence of powerful yet automated
abstraction techniques such as predicate abstraction. However, the
state-space explosion problem in model checking remains the chief
obstacle to the practical verification of real-world distributed
systems. Even in the case of purely sequential programs, a crucial
requirement to make predicate abstraction effective is to use as few
predicates as possible. This is because, in the worst case, the state
space of the abstraction generated (and consequently the time and
memory complexity of the abstraction process) is exponential in the
number of predicates involved. In addition, for concurrent programs,
the number of reachable states could grow exponentially with the
number of components.
We attempt to address these issues 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 (predicate abstraction for data and
action-guided abstraction for 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. Additionally, a key feature of our approach is that if a
property can be proven to hold or not hold based on a given finite set
of predicates P, the predicate refinement procedure we propose
in this article finds automatically a minimal subset of
P that is sufficient for the proof. This, along with 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 experimental results obtained with
our tool MAGIC.
Formal Methods in System Design 25(2-3), 2004. 46 pages.
PostScript / PDF
© 2004 Kluwer Academic Publishers.