This project is exploring a class of verification methods, called design reductions, which have advantages over conventional approaches. Design reduction works by simplifying a design incrementally. At each step, consistency checking is done using symbolic verification methods, which use symbolic simulation and automatic decision procedures for fragments of logic. For example, initial design reductions are proposed to remove pipelining and similar optimizations, eliminate caching, simplify interfaces, and eliminate traps and interrupts. Once a design has been simplified as much as possible, it can be compared with a user-supplied specification much more easily than can the original design. The project is also investigating several promising avenues to avoid or simplify the generation of inductive invariants, which is the most time-consuming aspect of symbolic verification. The project is searching for: new proof methods that only require invariants for certain states where the invariants are comparatively simple to express; ways of identifying internal correctness conditions that contribute to an invariant; and methods integrating approximate model checking into a more general framework.
