Computer Aided Verification
20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings
Page
%P
-
Chapter and Conference Paper
Verification of Computer Switching Networks: An Overview
Formal verification has seen much success in several domains of hardware and software design. For example, in hardware verification there has been much work in the verification of microprocessors (e.g. [1]) an...
-
Chapter and Conference Paper
Runtime Verification: A Computer Architecture Perspective
A major challenge in hardware verification is managing the state explosion problem in pre-silicon verification. This is seen in the high cost and low coverage of simulation, and capacity limitations of formal ...
-
Chapter and Conference Paper
Parallel Assertions for Architectures with Weak Memory Models
Assertions are a powerful and widely used debugging tool in sequential programs, but are ineffective at detecting concurrency bugs. We recently introduced parallel assertions which solve this problem by provid...
-
Chapter and Conference Paper
Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search
In our recent work, we addressed the problem of detecting serializability violations in a concurrent program using predictive analysis, where we used a graph-based method to derive a predictive model from a gi...
-
Chapter and Conference Paper
Parameterized Model Checking of Fine Grained Concurrency
Concurrent data structures are provided in libraries such as Intel Thread Building Blocks and Java.util.concurrent to enable efficient implementation of multi-threaded programs. Their efficiency is achieved by...
-
Article
Specification and encoding of transaction interaction properties
Transaction-level modeling is used in hardware design for describing designs at a higher level compared to the register-transfer level (RTL) (e.g. Cai and Gajski in CODES+ISSS ’03: proceedings of the 1st IEEE/...
-
Article
Preface
-
Article
Declarative Infrastructure Configuration Synthesis and Debugging
There is a large conceptual gap between end-to-end infrastructure requirements and detailed component configuration implementing those requirements. Today, this gap is manually bridged so large numbers of conf...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Hardware Verification: Techniques, Methodology and Solutions
Hardware verification has been one of the biggest drivers of formal verification research, and has seen the greatest practical impact of its results. The use of formal techniques has not been uniformly success...
-
Chapter and Conference Paper
Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares
Traditionally the propositional part of a Quantified Boolean Formula (QBF) instance has been represented using a conjunctive normal form (CNF). As with propositional satisfiability (SAT), this is motivated by ...
-
Chapter and Conference Paper
Lemma Learning in SMT on Linear Constraints
The past decade has seen great improvement in Boolean Satisfiability(SAT) solvers. SAT solving is now widely used in different areas, including electronic design automation, software verification and artificia...
-
Chapter and Conference Paper
On Solving the Partial MAX-SAT Problem
Boolean Satisfiability (SAT) has seen many successful applications in various fields such as Electronic Design Automation and Artificial Intelligence. However, in some cases, it may be required/preferable to u...
-
Chapter and Conference Paper
A Case for Runtime Validation of Hardware
Increasing hardware design complexity has resulted in significant challenges for hardware design verification. The growing “verification gap” between the complexity of what we can verify and what we can fabric...
-
Article
Achieving Structural and Composable Modeling of Complex Systems
This paper describes a recently released, structural and composable modeling system called the Liberty Simulation Environment (LSE). LSE automatically constructs simulators from system descriptions that closel...
-
Chapter and Conference Paper
Symmetry Reduction in SAT-Based Model Checking
The major challenge facing model checking is the state explosion problem. One technique to alleviate this is to apply symmetry reduction; this exploits the fact that many sequential systems consist of intercha...
-
Chapter and Conference Paper
Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems
The sequential circuit state space diameter problem is an important problem in sequential verification. Bounded model checking is complete if the state space diameter of the system is known. By unrolling the t...
-
Chapter and Conference Paper
Zchaff2004: An Efficient SAT Solver
The Boolean Satisfiability Problem (SAT) is a well known NP-Complete problem. While its complexity remains a source of many interesting questions for theoretical computer scientists, the problem has found many...
-
Chapter and Conference Paper
Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms
We experimentally evaluate the cache performance of different SAT solvers as a case study for the efficient implementation of SAT algorithms. We evaluate several different Boolean Constraint Propagation (BCP) ...
-
Chapter
Modeling and Integration of Peripheral Devices in Embedded Systems
This paper describes automation methods for device driver development in IP-based embedded systems in order to achieve high reliability, productivity, reusability and fast time to market. We formally specify d...
