Report Number: CS-TR-99-1618
Institution: Stanford University, Department of Computer Science
Title: Abstraction-based Deductive-Algorithmic Verification of
Author: Uribe, Tomas E.
Date: March 1999
Abstract: This thesis presents a framework that combines deductive and
algorithmic methods for verifying temporal properties of
reactive systems, to allow more automatic verification of
general infinite-state systems and the verification of larger
finite-state ones. Underlying these methods is the theory of
property-preserving assertion-based abstractions, where a
finite-state abstraction of the system is deductively
justified and algorithmically model checked.
After presenting an abstraction framework that accounts for
fairness, we describe a method to automatically generate
finite-state abstractions. We then show how a number of other
verification methods, including deductive rules,
(Generalized) Verification Diagrams, and Deductive Model
Checking, can also be understood as constructing finite-state
abstractions that are model checked.
Our analysis leads to a better classification and
understanding of these verification methods. Furthermore, it
shows how the different abstractions that they construct can
be combined. For this, we present an algorithmic Extended
Model Checking procedure, which uses all the information that
these methods produce, in a finite-state format that can be
easily and incrementally combined. Besides a standard safety
component, the combined abstractions include extra bounds on
fair transitions, well-founded orders, and constrained
transition relations for the generation of counterexamples.
Thus, our approach minimizes the need for user interaction
and maximizes the impact of the available automated deduction
and model checking tools. Once proved, verification
conditions are re-used as much as possible, leaving the
temporal and combinatorial reasoning to automatic tools.