-
Chapter and Conference Paper
A Partitioning Methodology for BDD-Based Verification
The main challenge in BDD-based verification is dealing with the memory explosion problem during reachability analysis. In this paper we advocate a methodology to handle this problem based on state space parti...
-
Chapter and Conference Paper
Evolution as Design Engineer
Exponential growth in digital information gathering, storage, and processing capabilities for biological data herald a new age of biology, when entire biological systems can potentially be understood. In order...
-
Chapter and Conference Paper
Strengthening Invariants by Symbolic Consistency Testing
We describe a relatively simple method for strengthening invariants when verifying infinite-state hardware systems called symbolic consistency testing. The method requires a high-level symbolic simulator and a de...
-
Chapter and Conference Paper
Semi-formal Verification of Memory Systems by Symbolic Simulation
We propose a debugging method for data-path intensive systems, in particular, memory systems. The approach is based on strengthening invariants by deriving constraints on data in the design using symbolic simu...
-
Chapter and Conference Paper
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic
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 theories like ...
-
Article
Efficient algorithms for approximate time separation of events
Finding bounds on time separation of events is a fundamental problem in the verification and analysis of asynchronous and concurrent systems. Unfortunately, even for systems without repeated events or choice, ...
-
Article
Formal Verification of Out-of-Order Execution with Incremental Flushing
We present an approach for formally verifying that a high-level microprocessor model behaves as defined by an instruction-set architecture. The technique is based on a specialization of self consistency called in...
-
Chapter and Conference Paper
CVC: A Cooperating Validity Checker
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 implements a ...
-
Chapter and Conference Paper
Counter-Example Based Predicate Discovery in Predicate Abstraction
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 the user t...
-
Chapter and Conference Paper
Faster Proof Checking in the Edinburgh Logical Framework
This paper describes optimizations for checking proofs represented in the Edinburgh Logical Framework (LF). The optimizations allow large proofs to be checked efficiently which cannot feasibly be checked using...
-
Chapter and Conference Paper
Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT
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 certain s...
-
Chapter and Conference Paper
Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods
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,2,19], we tran...
-
Chapter and Conference Paper
A Generalization of Shostak#x2019;s Method for Combining Decision Procedures
Consider the problem of determining whether a quantifier-free formula ϕ is satisfiable in some first-order theory T . Shostak#x2019;s algorithm decides this problem for a certain class of theories with both inter...
-
Article
Parallelizing the Murϕ Verifier
With the use of state and memory reduction techniques in verification by explicit state enumeration, runtime becomes a major limiting factor. We describe a parallel version of the explicit state enumeration ve...
-
Chapter and Conference Paper
A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® Itanium™ Processor Bus Protocol
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 documented informal...
-
Chapter and Conference Paper
Monitor-Based Formal Specification of PCI
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 in use ar...
-
Chapter and Conference Paper
A Framework for Cooperating Decision Procedures
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 Nelson and Oppen...
-
Chapter and Conference Paper
Symbolic Simulation with Approximate Values
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 simulation is a me...
-
Article
Verifying Systems with Replicated Components in Murϕ
An extension to the Murϕ verifier is presented to verify systems with replicated identical components. Although most systems are finite-state in nature, many of them are also designed to be scalable, so that a...
-
Chapter and Conference Paper
Alternative Approaches to Hardware Verification
BDD-based symbolic model checking has received a great deal of attention because of its potential for solving hardware verification problems. However, there are other, qualitatively different, approaches that ...
