PDPAR 2004 Preliminary Version (2004)
Cvc Lite, Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, ...
Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been...
Cmc: A Model Checker For Network (2004)
Complex systems have complex errors. Real systems have a variety of mishandled corner cases triggered by intricate sequences of events. In practice, this leaves a residue of errors that cause system...
Combination Results for Many Sorted (2004)
Vijay Ganesh, Sergey Berezin, Cesare Tinelli, David L. Dill
We present a combination result for many-sorted rst-order theories whose signatures may share common symbols (i.e. overlapping or non-disjoint signatures), extending the recent results by Ghilardi...
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic (2003)
Sergey Berezin, Vijay Ganesh, David L. Dill
Efficient decision procedures for arithmetic play a very important role in formal verification. In practical examples, however, arithmetic constraints are often mixed with constraints from other...
Strengthening Invariants by Symbolic Consistency Testing (2003)
Husam Abu-haimed, Sergey Berezin, David L. Dill
We describe a relatively simple method for strengthening invariants when verifying in nite-state hardware systems called symbolic consistency testing. The method requires a high-level symbolic...
CMC: A Pragmatic Approach to Model Checking Real Code (2003)
Madanlal Musuvathi, Andy Chou, Dawson R. Engler, David L. Dill
Many system errors do not emerge unless some intricate sequence of events occurs. In practice, this means that most systems have errors that only trigger after days or weeks of execution. Model...
Draft. Please do not distribute] (2002)
Sergey Berezin, Vijay Ganesh, David L. Dill
Efficient decision procedures for arithmetic play a very important role in formal verification. In practical examples, however, arithmetic constraints are often mixed with constraints from other...
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods (2002)
Vijay Ganesh, Sergey Berezin, David L. Dill
We present a new way of using Binary Decision Diagrams in automata based algorithms for solving the satisfiability problem of quantifier-free Presburger arithmetic. Unlike in previous approaches [5,...
Deciding Presburger Arithmetic by Model Checking (2002)
Vijay Ganesh, Sergey Berezin, David L. Dill
We present a new way of using Binary Decision Diagrams in automata based algorithms for solving the satisfiability problem of quantifier-free Presburger arithmetic. Unlike in previous approaches [5,...
CMC: A Pragmatic Approach to Model Checking Real Code (2002)
Madanlal Musuvathi, Andy Chou, Dawson R. Engler, David L. Dill
Many system errors do not emerge unless some intricate sequence of events occurs. In practice, this means that most systems have errors that only trigger after days or weeks of execution. Model...
A Generalization of Shostak's Method for (2002)
Clark W. Barrett, David L. Dill, Aaron Stump
Consider the problem of determining whether a quantifierfree formula OE is satisfiable in some first-order theory T . Shostak's algorithm decides this problem for a certain class of theories with...
Checking Satisfiability of First-Order Formulas (2002)
Clark W. Barrett, David L. Dill, Aaron Stump
In the past few years, general-purpose propositional satisfiability (SAT) solvers have improved dramatically in performance and have been used to tackle many new problems. It has also been shown that...
Counter-Example Based Predicate Discovery in Predicate Abstraction (2002)
The application of predicate abstraction to parameterized systems requires the use of quantified predicates. These predicates cannot be found automatically by existing techniques and are tedious for...
CVC: a Cooperating Validity Checker (2002)
Aaron Stump, Clark W. Barrett, David L. Dill
Decision procedures for decidable logics and logical theories have proven to be useful tools in verification. This paper describes the CVC ("Cooperating Validity Checker") decision procedure. CVC...
Faster Proof Checking in the Edinburgh Logical Framework (2002)
This paper describes optimizations for checking proofs represented in the Edinburgh Logical Framework (LF). The optimizations allow large proofs to be checked eciently which cannot feasibly be...
Deriving a Simulation Input Generator and a Coverage (2002)
This paper presents novel uses of functional interface specifications for verifying RTL designs. We demonstrate how a simulation environment, a correctness checker, and a functional coverage metric...
Deriving a Simulation Input Generator and a Coverage Metric From a Formal Specification (2002)
This paper presents novel uses of functional interface specifications for verifying RTL designs. We demonstrate how a simulation environment, a correctness checker, and a functional coverage metric...
A Decision Procedure for an Extensional Theory of Arrays (2001)
Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy Levitt
A decision procedure for a theory of arrays is of interest for applications in formal verification, program analysis, and automated theorem-proving. This paper presents a decision procedure for an...
A Decision Procedure for an Extensional Theory of Arrays (2001)
Aaron Stump, Clark W. Barrett, David L. Dill
A decision procedure for a theory of arrays is of interest for applications in formal verification, program analysis, and automated theorem-proving. This paper presents a decision procedure for an...
Symbolic Simulation Using Automatic Abstraction of Internal Node Values (2001)
James Christopher Wilson, David L. Dill
In recent years, veri cation has emerged as a major portion of the eort in designing large, complex chips. Simulation-based methods such as directed and random testing are the most widely used veri...
Flea: a Fast Proof Checker for Elliptical LF (2001)
Proof checkers are crucial components in several dierent areas of Computer Science. Proof-carrying code and proof-carrying authentication require a proof checker to check proofs that mobile code is...
Proof Production in Decision Procedures (2001)
Aaron Stump, Clark W. Barrett, David L. Dill, Cormac Flanagan
Software that can produce independently checkable evidence for the correctness of its output has received recent attention for use in certifying compilers and proof-carrying code. This paper...
Self-Timed Logic Using Current-Sensing Completion Detection (CSCD) (2001)
This article proposes a completion-detection method for efficiently implementing Boolean functions as self-timed logic structures. Current-Sensing Completion Detection, CSCD, allows self-timed...
Kanna Shimizu, David L. Dill, Ching-tsun Chou
In practice, formal specifications are often considered too costly for the benefits they promise. Specifically, interface specifications such as standard bus protocol descriptions are still...
A Simple Method for Extracting Models from Protocol Code (2001)
David Lie, Andy Chou, Dawson Engler, David L. Dill
The use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result, verification is rarely used...
Efficient Algorithms for Approximate Time Separation of Events (2001)
Supratik Chakraborty, David L. Dill, Kenneth Y. Yun
Finding bounds on time separation of events is a fundamental problem in verification and analysis of asynchronous and concurrent systems. Unfortunately, even for systems without repeated events or...
Formal Verification of the TORCH Microprocessor RTL Design (2001)
Jeffrey Su, Laurent Arditi, Satyaki Das, Jens U. Skakkebaek, David L. Dill
Given current design practices, practical verification of microprocessor designs requires checking
Clark W. Barrett, David L. Dill, Aaron Stump
Consider the problem of determining whether a quantifierfree formula OE is satisfiable in some first-order theory T with equality.
A Simple Method for Extracting Models from Protocol Code (2001)
David Lie, Andy Chou, Dawson Engler, David L. Dill
The use of model checking for validation requires that models of the underlying system be created. Creating such models is difficult and error prone and as a result, verification is rarely used...
A Simple Method for Extracting Models from Protocol Code (2001)
David Lie, Andy Chou, Dawson Engler, David L. Dill
The use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result, verification is rarely used...
Symbolic Simulation with Approximate Values (2000)
Chris Wilson, David L. Dill, Al E. Bryant
. Symbolic methods such as model checking using binary decision diagrams (BDDs) have had limited success in verifying large designs because BDD sizes regularly exceed memory capacity. Symbolic...
Reliable Verification Using Symbolic Simulation with Scalar Values (2000)
This paper presents an algorithm for hardware verification that uses simulation and satisfiability checking techniques to determine the correctness of a symbolic test case on a circuit. The goal is...
Polynomial-Time Techniques For Approximate Timing Analysis Of Asynchronous Systems (2000)
David L. Dill, Giovanni De Micheli, Kenneth Y. Yun, Krishna Saraswat
As designers strive to build systems on chips with ever diminishing device sizes, and as clock speeds of gigahertz and above are being contemplated, the limitations of synchronous circuits are...
Monitor-Based Formal Specification of PCI (2000)
Kanna Shimizu, David L. Dill, Alan J. Hu
. Bus protocols are hard to specify correctly, and yet it is often critical and highly beneficial that their specifications are correct, complete, and unambiguous. The informal specifications...
Validation Tools for Complex Digital Designs (2000)
David L. Dill, Oyekunle Olukotun
iv Acknowledgments vi Table of Contents vii List of Tables x List of Figures xi Chapter 1.
Monitor-Based Formal Specification of PCI (2000)
Kanna Shimizu, David L. Dill, Alan J. Hu
Bus protocols are hard to specify correctly, and yet it is often critical and highly beneficial that their specifications are correct, complete, and unambiguous. The informal specifications currently...
Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking (2000)
Shankar G. Govindaraju, David L. Dill
BDD-based symbolic techniques of approximate reachability analysis based on decomposing the circuit into a collection of overlapping sub-machines (also referred to as overlapping projections) have...
David Y. W, Park Ulrich, Stern Jens, U. Skakkebk, David L. Dill
This paper presents initial results in model checking multi-threaded Java programs. Java programs are translated into the SAL (Symbolic Analysis Laboratory) intermediate language, which supports...
Experience with Predicate Abstraction (2000)
ion ? Satyaki Das 1 , David L. Dill 1 , and Seungjoon Park 2 1 Computer Systems Laboratory, Stanford University, Stanford, CA 94305 2 RIACS, NASA Ames Research Center, Moffett Field, CA 94035...
An Executable Specification and Verifier for Relaxed Memory Order (2000)
The Mur# description language and verification system for finite-state concurrent systems is applied to the problem of specifying a family of multiprocessor memory models described in the SPARC...
A Framework for Cooperating Decision Procedures (2000)
Clark W. Barrett, David L. Dill, Aaron Stump
. We present a flexible framework for cooperating decision procedures. We describe the properties needed to ensure correctness and show how it can be applied to implement an efficient version of...
Reliable Verification Using Symbolic Simulation with Scalar Values (2000)
This paper presents an algorithm for hardware verification that uses simulation and satisfiability checking techniques to determine the correctness of a symbolic test case on a circuit. The goal is...
Timing Analysis of Asynchronous Systems Using Time Separation of Events (2000)
Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
This paper describes a pseudo-polynomial time algorithm for timing analysis of a class of choice-free asynchronous systems, called tightly-coupled systems, with both min and max type timing...
Practical Timing Analysis of Asynchronous Circuits Using Time Separation of Events (2000)
Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
We present a unified technique for timing verification and performance analysis of complex asynchronous circuits designed with implicit timing assumptions. We model interacting asynchronous...
Approximate Time Separation of Events in Practice (2000)
Supratik Chakraborty, Pasupathi A. Subrahmanyam, David L. Dill
Finding bounds on the time separations between events is a fundamental problem in the analysis of concurrent systems. In [4], we proposed a polynomial-time approximate algorithm for computing bounds...
Practical Timing Analysis of Asynchronous Systems Using Time Separation of Events (2000)
Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
We present a unified technique for timing verification and performance analysis of complex asynchronous systems designed with implicit timing assumptions. Our method models interacting controllers...
Min-Max Timing Analysis and An Application to Asynchronous Circuits (2000)
Supratik Chakraborty, David L. Dill, Kenneth Y. Yun, Member Ieee
Modern high-performance asynchronous circuits depend on timing constraints for correct operation, so timing analyzers are essential asynchronous design tools. In this paper, we present a 13-valued...
Timing Analysis for Extended Burst-Mode Circuits (2000)
Supratik Chakraborty, David L. Dill, Kenneth Y. Yun, Kun-yung Chang
We describe an efficient timing analysis technique for extended burst-mode circuits implemented according to the 3D design style. Gate-level 3D circuits with uncertain component delays are analyzed,...
More Accurate Polynomial-Time Min-Max Timing Simulation (2000)
Supratik Chakraborty, David L. Dill
We describe a polynomial-time algorithm for min-max timing simulation of combinational circuits. Our algorithm reports conservative bounds on the propagationdelays from each primary input to each...
Approximate Algorithms for Time Separation of Events (2000)
Supratik Chakraborty, David L. Dill
We describe a polynomial-time approximate algorithm for computing minimum and maximum time separations between all pairs of events in systems specified by acyclic timing constraint graphs. Even for...
Polynomial-Time Techniques For Approximate Timing Analysis Of Asynchronous Systems (2000)
Supratik Chakraborty, David L. Dill, Krishna Saraswat
As designers strive to build systems on chips with ever diminishing device sizes, and as clock speeds of gigahertz and above are being contemplated, the limitations of synchronous circuits are...
Reliable Verification Using Symbolic Simulation with Scalar Values (2000)
This paper presents an algorithm for hardware verification that uses simulation and satisfiability checking techniques to determine the correctness of a symbolic test case on a circuit. The goal is...
Exact Two-Level Minimization of Hazard-Free Logic with Multiple-Input Changes (1999)
Steven M. Nowick, David L. Dill
This paper describes a new method for exact hazard-free logic minimization of Boolean functions. Given an incompletely-specified Boolean function, the method produces a minimum-cost sum-ofproducts...
Design and Analysis of Design and Analysis of Communication Software Communication Software (1999)
David L. Dill, Patrice Godefroid
Introduction -- Part 3 - Model-Checking Software using VeriSoft (Sep 30) . A New Approach to Communication Software Analysis -- Part 4 - Inside VeriSoft (Oct 14 & 21) . The Research Behind The Tool...
Approximate Symbolic Model Checking using Overlapping Projections (1999)
Shankar G. Govindaraju, David L. Dill
Symbolic Model Checking extends the scope of verification algorithms that can be handled automatically, by using symbolic representations rather than explicitly searching the entire state space of...
Generating Proofs from a Decision Procedure (1999)
Fully automatic decision procedures are used to improve performance in many different applications of formal verification. In most cases, the decision procedures are treated as trusted components of...
Experience with Predicate Abstraction (1999)
ion ? Satyaki Das 1 , David L. Dill 1 , and Seungjoon Park 2 1 Computer Systems Laboratory, Stanford University, Stanford, CA 94305 2 RIACS, NASA Ames Research Center, Moffett Field, CA 94035...
Experience with Predicate Abstraction (1999)
ion ? Satyaki Das 1 , David L. Dill 1 , and Seungjoon Park 2 1 Computer Systems Laboratory, Stanford University, Stanford, CA 94305 2 RIACS, NASA Ames Research Center, Moffett Field, CA 94035...
Improved Approximate Reachability using Auxiliary State Variables (1999)
Shankar G. Govindaraju, David L. Dill, Jules P. Bergmann
Approximate reachability techniques trade off accuracy for the capacity to deal with bigger designs. Cho et al [4] proposed partitioning the set of state bits into mutually disjoint subsets and doing...
Formally Verifying Data and Control with Weak Reachability Invariants (1999)
Jeffrey Su, David L. Dill, Jens U. Skakkebæk
. Existing formal verification methods do not handle systems that combine state machines and data paths very well. Model checking deals with finitestate machines efficiently, but model checking full...
Timing Analysis of Asynchronous Systems Using Time Separation of Events (1999)
Supratik Chakraborty, Kenneth Y. Yun, David L. Dill
This paper describes a pseudo-polynomial time algorithm for timing analysis of a class of choice-free asynchronous systems, called tightly-coupled systems, with both min and max type timing...
Min-Max Timing Analysis and An Application to Asynchronous Circuits (1999)
Supratik Chakraborty, David L. Dill, Member Ieee, Kenneth Y. Yun
Modern high-performance asynchronous circuits depend on timing constraints for correct operation, so timing analyzers are essential asynchronous design tools. In this paper, we present a 13-valued...
Formally Verifying Data and Control With Weak Reachability Invariants (1998)
Su, Jeffrey, Dill, David L., Skakkebaek, Jens U.
Existing formal verification methods do not handle systems that combine state machines and data paths very well. Model checking deals with finite-state machines efficiently, but model checking full...
Static Analysis to Identify Invariants in RSML Specifications (1998)
Park, David Y., Skakkebaek, Jens U., Dill, David L.
Static analysis of formal, high-level specifications of safety critical software can discover flaws in the specification that would escape conventional syntactic and semantic analysis. As an example,...
Checking Properties of Safety Critical Specifications Using Efficient Decision Procedures (1998)
Park, David Y., Skakkebaek, Jens U., Heimdahl, Mats P., Czerny, Barbara J., Dill, David L.
The increasing use of software in safety critical systems entails increasing complexity, challenging the safety of these systems. Although formal specifications of real-life systems are orders of...
A Decision Procedure for Bit-Vector Arithmetic (1998)
Barrett, Clark W., Dill, David L., Levitt, Jeremy R.
Bit-vector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although...
Formal Verification of Out-of-Order Execution Using Incremental Flushing (1998)
Skakkebaek, Jens U., Jones, Robert B., Dill, David L.
We present a two-part approach for verifying out-of-order execution. First, the complexity of out-of-order issue and scheduling is handled by creating an in-order abstraction of the out-of-order...
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution (1998)
Jones, Robert B., Skakkebaek, Jens U., Dill, David L.
Several methods have recently been proposed for verifying processors with out-of-order execution. These methods use intermediate abstractions to decompose the verification process into smaller steps....
Approximate Reachability With BDDs Using Overlapping Projections (1998)
Govindaraju, Shankar G., Dill, David L., Hu, Alan J., Horowitz, Mark A.
Approximate reachability techniques trade off accuracy with the capacity to deal with bigger designs. Cho et al proposed approximate FSM traversal algorithms over a partition of the set of state...
A Federal Approach to Formal Hardware Design Verification (1998)
The goal of this project was to enable the solution of hard formal verification problems - and thereby reduce the cost and improve the quality of advanced hardware designs - by making it possible to...
Approximate Symbolic Model Checking Using Overlapping Projections (1998)
Govindaraju, Shankar G., Dill, David L.
Abstract Symbolic Model Checking extends the scope of verification algorithms that can be handled automatically, by using symbolic representations rather than explicitly searching the entire state...
A Simple Method for Extracting Models from Protocol Code (1998)
Lie, David, Chou, Andy, Engler, Dawson, Dill, David L.
The use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result verification is rarely used...
Verification by Approximate Forward and Backward Reachability (1998)
Shankar G. Govindaraju, David L. Dill
Approximate reachability techniques trade off accuracy for the capacity to deal with bigger designs. In this paper, we extend the idea of approximations using overlapping projections to symbolic...
Approximate Reachability with BDDs using Overlapping Projections (1998)
Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark A. Horowitz
Approximate reachability techniques trade off accuracy with the capacity to deal with bigger designs. Cho et al [3] proposed approximate FSM traversal algorithms over a partition of the set of state...
Approximate Reachability with BDDs using Overlapping Projections (1998)
Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark A. Horowitz
Approximate reachability techniques trade off accuracy with the capacity to deal with bigger designs. Cho et al [3] proposed approximate FSM traversal algorithms over a partition of the set of state...
Validation with Guided Search of the State Space (1998)
In practice, model checkers are most useful when they find bugs, not when they prove a property. However, because large portions of the state space of the design actually satisfy the specification,...
Approximate Reachability with BDDs using Overlapping Projections (1998)
Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark A. Horowitz
Approximate reachability techniques trade o# accuracy with the capacity to deal with bigger designs. Cho et al #3# proposed approximate FSM traversal algorithms over a partition of the set of state...
A Decision Procedure for Bit-Vector Arithmetic (1998)
Clark W. Barrett, David L. Dill, Jeremy R. Levitt
Bit-vector theories with concatenation and extraction have been shown to be useful and important for hardware veri- #cation. Wehave implemented an extended theory which includes arithmetic. Although...
Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution (1998)
Robert B. Jones, Jens U. Skakkebaek, David L. Dill
ion in Formal Verification of Out-of-Order Execution Robert B. Jones 1;2 , Jens U. Skakkebaek 1 , and David L. Dill 1 1 Computer Systems Laboratory, Stanford University, Stanford, CA 94305, USA...
Reducing Manual Abstraction in (1998)
Robert B. Jones, Jens U. Skakkebaek, David L. Dill
Several methods have recently been proposed for verifying processors with out-of-order execution. These methods use intermediate abstractions to decompose the verification process into smaller steps....
Verification by Approximate Forward and Backward Reachability (1998)
Shankar G. Govindaraju, David L. Dill
Approximate reachability techniques trade off accuracy for the capacity to deal with bigger designs. In this paper, we extend the idea of approx