-
Chapter and Conference Paper
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
In this work we propose to use Syntax-Guided Synthesis (SyGuS) for lemma generation in a word-level IC3/PDR framework for bit-vector problems. Hardware model checking is moving from bit-level to word-level pro...
-
Chapter and Conference Paper
Synthesizing Environment Invariants for Modular Hardware Verification
We automate synthesis of environment invariants for modular hardware verification in processors and application-specific accelerators, where functional equivalence is proved between a high-level specification ...
-
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
Post-Silicon Fault Localization with Satisfiability Solvers
This chapter covers techniques to localize faults in integrated circuits by means of automated satisfiability solvers. These techniques aim at identifying fault candidates for an erroneous execution trace by s...
-
Chapter
Propositional SAT Solving
The Boolean Satisfiability Problem (SAT) is well known in computational complexity, representing the first decision problem to be proved NP-complete. SAT is also often the subject of work in proof complexity. ...
-
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...
-
Chapter
Verifying Security Properties in Modern SoCs Using Instruction-Level Abstractions
This chapter describes a methodology for system-level security verification of modern Systems-on-Chip (SoC) designs. These designs comprise interacting intellectual property (IP) blocks which are often sourced...
-
Chapter and Conference Paper
IC3 - Flip** the E in ICE
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...
-
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
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
Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom
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
SAT Based Verification of Network Data Planes
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
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
Model Checking Unbounded Concurrent Lists
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
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
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 ...