Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs

摘要

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 state/event-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 state/event- 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.