Computer Aided Verification
20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings
Page
%P
23 Result(s)
-
Chapter and Conference Paper
ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions
We present ILAng, a platform for modeling and verification of systems-on-chip (SoCs) using Instruction-Level Abstractions (ILA). The ILA formal model targeting the hardware-software interface enables a clean s...
-
Chapter and Conference Paper
Lazy Self-composition for Security Verification
The secure information flow problem, which checks whether low-security outputs of a program are influenced by high-security inputs, has many applications in verifying security properties in programs. In this p...
-
Chapter and Conference Paper
Trace-based Analysis of Memory Corruption Malware Attacks
Understanding malware behavior is critical for cybersecurity. This is still largely done through expert manual analysis of the malware code/binary. In this work, we introduce a fully automated method for malwa...
-
Article
On computing minimal independent support and its applications to sampling and counting
Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions...
-
Chapter and Conference Paper
Reduction of Resolution Refutations and Interpolants via Subsumption
Propositional resolution proofs and interpolants derived from them are widely used in automated verification and circuit synthesis. There is a broad consensus that “small is beautiful”—small proofs and interpo...
-
Chapter and Conference Paper
Coverage-Based Trace Signal Selection for Fault Localisation in Post-silicon Validation
Post-silicon validation is the time-consuming process of detecting and diagnosing defects in prototype silicon. It targets electrical and functional defects that escaped detection during pre-silicon verificati...
-
Chapter and Conference Paper
Modeling Firmware as Service Functions and Its Application to Test Generation
The term firmware refers to software that is tied to a specific hardware platform, e.g., low-level drivers that physically interface with the peripherals. More recently, this has grown to include software that...
-
Chapter and Conference Paper
passert: A Tool for Debugging Parallel Programs
passert is a new debugging tool for parallel programs which allows programmers to express correctness criteria using a simple, expressive assertion language. We demonstrate how these parallel assertions allow the...
-
Chapter and Conference Paper
Wolverine: Battling Bugs with Interpolants
Wolverine is a software verifier that checks safety properties of sequential ANSI-C and C++ programs, deploying Craig interpolation to derive program invariants. We describe the underlying approa...
-
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...
-
Book and Conference Proceedings
-
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
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 and Conference Paper
The Quest for Efficient Boolean Satisfiability Solvers
The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enab...
-
Chapter and Conference Paper
Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation
In this paper, we describe a new framework for evaluating Quantified Boolean Formulas (QBF). The new framework is based on the Davis-Putnam (DPLL) search algorithm. In existing DPLL based QBF algorithms, the p...
