-
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
Fast Interpolating BMC
Bounded Model Checking (BMC) is well known for its simplicity and ability to find counterexamples. It is based on the idea of symbolically representing counterexamples in a tr...
-
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...
-
Article
Preface
-
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
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
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
Optimal Live Range Merge for Address Register Allocation in Embedded Programs
The increasing demand for wireless devices running mobile applications has renewed the interest on the research of high performance low power processors that can be programmed using very compact code. One way ...
-
Chapter and Conference Paper
Exploiting Retiming in a Guided Simulation Based Validation Methodology
There has been much interest recently in combining the strengths of formal verification techniques and simulation for functional validation of large designs [6].Typically, a formal test model is first obtained fr...
-
Chapter and Conference Paper
Cinderella: A retargetable environment for performance analysis of real-time software
Real-time systems are characterized by the presence of timing constraints that a task must be completed within a given deadline. In this paper, we present a complete environment for determining best-case and w...
