A Counterexample Guided Abstraction

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 e#ciently 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 statespa..