A Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Pagination or Media Count:
This dissertation presents a framework for verifying concurrent message-passing C programs in an automated manner. First, programs are modeled as finite state machines whose states are labeled with data and whose transitions are labeled with events. The author refers to such state machines as labeled Kripke structures LKSs. His stateevent-based approach enables him to succinctly express and efficiently verify properties that involve simultaneously both the static data-based and the dynamic reactive or event-based aspects of any software system. Second, the framework supports a wide range of specification mechanisms and notions of conformance i.e., complete system specifications can be expressed as LKSs and simulation conformance verified between such specifications and any C implementation. For partial specifications, the framework supports in addition to LKSs a stateevent-based linear temporal logic capable of expressing complex safety as well as liveness properties. The framework enables one to check for deadlocks in concurrent message-passing programs. Third, for each notion of conformance, the author presents a completely automated and compositional verification procedure based on the counterexample guided abstraction refinement CEGAR paradigm. These verification procedures consist of an iterative application of model construction, model checking, counterexample validation, and model refinement steps. However, they are uniquely distinguished by their compositionality. In each of his conformance checking procedures, the algorithms for model construction, counterexample validation, and model refinement are applied component-wise. The statespace size of the models are controlled via a two-pronged strategy 1 using two complementary abstraction techniques based on the static predicate abstraction and dynamic action-guided abstraction aspects of the program, and 2 minimizing the number of predicates required for predicate abstraction.
- Computer Programming and Software