Ecien t Verication of Sequential and Concurrent C
Karen Yorav · 2004
There has been considerable progress in the domain of software verica- tion 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 verication of real-world distributed systems. Even in the case of purely sequential programs, a crucial requirement to make predicate abstraction eectiv e 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 specications. More specically , 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 renemen t scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specication is either established or refuted. Additionally, a key feature of our approach is that if a property can be proved to hold or not hold based on a given nite set of predicates P, the predicate renemen t procedure we propose in this article nds automatically a minimal subset of P that is sucien t 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.