Where deduction meets exploration

These are two approaches to the formal verification of invariance properties of reactive designs (i.e., reactive programs or digital circuit designs). They both show that all states that can arise in a behaviour of the system described by the design satisfy a given state property, such as mutual exclusion, etc. The explorative approach (model checking), applied to a finite state system, generates first the set of all reachable states, and then checks that all of them satisfy the state property of interest. A competing approach is that of Deductive Verification, in which the validity of a temporal property of a design is proved as a mathematical theorem, conducted within a theorem-proving support system such as HOL, PVS, or STeP.

After describing these two approaches to verification, we will present some approaches for bridging the gap between the two, hopefully getting the best of the two methods while overcoming their respective weaknesses. Technically, we propose Symbolic Model Checking with (rich) assertional languages that can describe infinite sets of states. The two examples that were worked out in detail and implemented are the language of regular expressions and the language of tree regular expressions. With these two languages, we were able to automatically verify networks of processes arranged along a linear array, a ring, and a tree. In particular, the method enabled us to verify the design of the FutureBus+ for arbitrary (and infinitely many) configurations. This extension of the explorative method towards infinite-state systems can also be viewed as identification of cases in which the deductive method can be applied in a fully automatic manner. In the talk, we will establish this dual view of progress in these two areas.