STeP-Related:
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 deductive-algorithmic 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 methods, including deductive rules, (Generalized) Verification Diagrams, and Deductive Model Checking, can also be understood as constructing finite-state versions of the system that are model checked.
This 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 abstract model checking procedure, which uses all the information produced by these methods, expressed 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 reused as much as possible, leaving the temporal and combinatorial reasoning to automatic tools.
Generalized Verification Diagrams combine deductive and algorithmic verification to establish general temporal properties of finite- and infinite-state reactive systems. The diagram serves as an abstraction of the system. This abstraction is deductively justified and algorithmically model checked. We present a new simple class of verification diagrams, using Muller acceptance conditions, and show how they can be used to verify general temporal properties of reactive systems.
We review a number of temporal verification techniques for reactive systems using modularity and abstraction. Their use allows the verification of larger systems, and the incremental verification of systems as they are developed and refined. In particular, we show how deductive verification tools, and the combination of finite-state model checking and abstraction, allow the verification of infinite-state systems featuring data types commonly used in software specifications, including real-time and hybrid systems.
We present an algorithm that uses decision procedures to generate finite-state abstractions of possibly infinite-state systems. The algorithm compositionally abstracts the transitions of the system, relative to a given, fixed set of assertions. Thus, the number of validity checks is proportional to the size of the system description, rather than the size of the abstract state-space. The generated abstractions are weakly preserving for universal CTL* temporal properties. We describe several applications of the algorithm, implemented using the decision procedures of the Stanford Temporal Prover (STeP).
We present a procedure for proving the validity of first-order formulas in the presence of decision procedures for an interpreted subset of the language. The procedure is designed to be practical: formulas can have large complex boolean structure, and include structure sharing in the form of let- expressions. The decision procedures are only required to decide the unsatisfiability of sets of literals. However, T-refuting substitutions are used whenever they can be computed; we show how this can be done for a theory of partial orders and equality. The procedure has been implemented as part of STeP, a tool for the formal verification of reactive systems. Although the procedure is incomplete, it eliminates the need for user interaction in the proof of many verification conditions.
We present a modular framework for proving temporal properties of real-time systems, based on clocked transition systems and linear-time temporal logic. We show how deductive verification rules, verification diagrams, and automatic invariant generation can be used to establish properties of real-time systems in this framework. We also discuss global and modular proofs of the branching-time property of non-Zenoness. As an example, we present the mechanical verification of the generalized railroad crossing case study using the Stanford Temporal Prover, STeP.
We describe diagram-based formal methods for verifying temporal properties of finite- and infinite-state reactive systems. These methods, which share a common background and tools, differ in the way they use automatic procedures within an interactive setting based on deduction. They can be used to produce a static proof object, or to perform incremental analysis of systems and specifications.
We present an extension of classical tableau-based model checking procedures to the case of infinite-state systems, using deductive methods in an incremental construction of the behavior graph. Logical formulas are used to represent infinite sets of states in an abstraction of this graph, which is repeatedly refined in the search for a counterexample computation, ruling out large portions of the graph before they are expanded to the state-level. This can lead to large savings, even in the case of finite-state systems. Only local conditions need to be checked at each step, and previously proven properties can be used to further constrain the search. Although the resulting method is not always automatic, it provides a flexible, general and complete framework that can integrate a diverse number of other verification tools.
We present a class of Ordered Binary Decision Diagrams, Differential \BDD{}s, and transformations Push-up and Delta over them. In addition to the ordinary node-sharing in normal BDD's, isomorphic substructures can be collapsed further in DeltaBDD's and their derived classes, forming a more compact representation of boolean functions. The elimination of isomorphic substructures coincides with the repetitive occurrences of small components in many applications of BDD's. The reduction is potentially exponential in the number of nodes and proportional to the number of variables, while operations on DeltaBDD's remain efficient.
We compare two prominent decision procedures for propositional logic: Ordered Binary Decision Diagrams (OBDD's) and the Davis-Putnam procedure. Experimental results indicate that the Davis-Putnam procedure outperforms OBDD's in hard constraint-satisfaction problems, while OBDD's are clearly superior for Boolean functional equivalence problems from the circuit domain, and, in general, problems that require the schematization of a large number of solutions that share a common structure. The two methods illustrate the different and often complementary strengths of constraint-oriented and search-oriented procedures.
A long version is available with extra experimental results.
This paper describes a new representation for sortal constraints and a unification algorithm for the corresponding constrained terms. Variables range over sets of terms described by systems of set constraints that can express limited inter-variable dependencies. These sets of terms are more general than regular tree languages, but are still closed under intersection. The new unification algorithm shows sorted unification to be decidable for a broad class of sorted signatures, which we call semi-linear, and, more generally, for sort theories with a least Herbrand model that can be represented using the new constraints. A finite representation of a complete set of well-sorted unifiers can always be found, even in those cases where this set is infinite.
This thesis describes a new representation for sortal constraints and a unification algorithm for the corresponding constrained terms. Variables range over sets of terms described by systems of set constraints, which can express limited inter-variable dependencies. These sets of terms are more general than regular tree languages, but are still closed under intersection. The new unification algorithm shows sorted unification to be decidable for a broad class of sorted signatures, which we call semi-linear, and, more generally, for sort theories with a least Herbrand model that can be represented using the new constraints. Even though the unification problem in question is NP-hard, the generality of the algorithm may allow for particular efficient implementations for more restricted theories. This unification algorithm can be integrated into any of a variety of deductive systems, resulting in a hybrid substitutional reasoner. As an example, the soundness and completeness of a resolution-based deductive system that uses the new unification procedure is proved.
STeP-Related:The Framework for Resolution-based Automated Proof Procedure Systems (FRAPPS) is a set of functions written in Common Lisp that facilitate the construction of a wide variety of resolution-based deductive systems. FRAPPS offers the basic functionality necessary to build such systems, freeing users from low-level implementation concerns. It is not intended for use in the construction of high-performance theorem provers, but rather to provide a modular and customizable system useful for rapid prototyping and experimentation in teaching and research.
The Stanford home page
The Computer Science Department home page
The Theory Division home page