Abstract
All the verification techniques used in previous lectures were based on an implicit representation of systems using Boolean, symbolic or numerical formulas. Explicit verification, on the other hand, is based on systematic exploration of the system under study, by explicit enumeration of its states and transitions. In practice, explicit verification has very different properties to implicit verification. For example, it works well on highly asynchronous systems such as communication protocols and distributed algorithms, which are often less well-suited to implicit verification, which performs very well on synchronous systems. On the other hand, it parallelizes well, which is not yet the case for implicit algorithms.
However, for explicit verification to be effective, it is essential to implement a number of delicate optimizations: efficient, very large cache systems to detect states that have already been visited, partial order reductions to avoid enumerating sequences of independent actions in all possible orders, abstract interpretation by hashcodes that do not handle collisions, systematic use of randomness, and so on.
The lecture presents explicit algorithms and their applications through two of the main systems in the field: SPIN, developed by G. Holtzmann at Bell Labs, and CADP, developed at Inria by H. Garavel, R. Mateescu and their team. SPIN is a compact system based on an easy-to-use, but relatively limited, specification language derived from C, whereas CADP takes the form of a large library of combinable algorithms managed by a scripting language. CADP takes as input specifications written in various algebraic computations of communicating processes, and solves problems of enumeration, equivalence by bisimulation, hierarchical proofs by compositional reductions, etc. Both SPIN and CADP have very active academic and industrial user groups.
