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
Induction is a key element of state-of-the-art verification techniques. Automatically synthesizing and verifying inductive invariants is at the heart of Model Checking of safety properties. In this paper, we stud...
Article
We present a model checking-based method for verifying list-based concurrent set data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received ...
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
We consider the problem of verifying deadlock freedom for symmetric cache coherence protocols. While there are multiple definitions of deadlock in the literature, we focus on a specific form of deadlock which ...
Chapter and Conference Paper
Formal verification has seen relatively less application in verifying computer networking infrastructure. This is in part due to the lack of clean layers of abstraction that enable design modeling and specific...
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
We present a model checking based method for verifying list-based concurrent data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received sign...
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
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
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
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
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
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...
Book and Conference Proceedings
20th International Conference, CAV 2008 Princeton, NJ, USA, July 7-14, 2008 Proceedings
Chapter and Conference Paper
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
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...