Computer Aided Verification
20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings
Chapter and Conference Paper
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
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...
Chapter and Conference Paper
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
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
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 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 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
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
20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings
Chapter and Conference Paper
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 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
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 ...