A 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. The methodology relies on several key ideas. First, programs are modeled as finite state machines whose states are labeled with data and whose transitions are labeled with events. We refer to such state machines as labeled Kripke structures (LKSs). Our state/event-based approach enables us to succinctly express and efficiently verify properties which 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. For instance, 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. Finally, the framework enables us to check for deadlocks in concurrent message-passing programs. Third, for each notion of conformance, we present a completely automated and compositional verification procedure based on the counterexample guided abstraction refinement (CEGAR) paradigm. Like other CEGAR-based approaches, 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 . More precisely, in each of our conformance checking procedures, the algorithms for model construction, counterexample validation and model refinement are applied component-wise. The state-space size of the models are controlled via a two-pronged strategy: (i) using two complementary abstraction techniques based on the static (predicate abstraction) and dynamic (action-guided abstraction) aspects of the program, and (ii) minimizing the number of predicates required for predicate abstraction. The proposed framework has been implemented in the MAGIC tool. We present experimental evaluation in support of the effectiveness of our framework in verifying non-trivial concurrent C programs against a rich class of specifications in an automated manner.