Despite several decades of research, the problem of formal verification of infinite-state
systems has resisted effective automation. We describe a system---Ivy---for interactively …

Distributed protocols such as Paxos play an important role in many computer systems.
Therefore, a bug in a distributed protocol may have tremendous effects. Accordingly, a lot of …

We describe a general framework c2i for generating an invariant inference procedure from
an invariant checking procedure. Given a checker and a language of possible invariants, c2i …

This paper surveys the work to date on Ivy, a language and a tool for the formal specification
and verification of distributed systems. Ivy supports deductive verification using automated …

We present GRASShopper, a tool for compositional verification of heap-manipulating
programs against user-provided specifications. What makes our tool unique is its decidable …

Separation logic (SL) is a widely used formalism for verifying heap manipulating programs.
Existing SL solvers focus on decidable fragments for list-like structures. More complex data …

We present Universal Property Directed Reachability (PDR∀), a property-directed semi-
algorithm for automatic inference of invariants in a universal fragment of first-order logic …

The natural proof technique for heap verification developed by Qiu et al.[32] provides a
platform for powerful sound reasoning for specifications written in a dialect of separation …

This paper addresses the problem of automatically generating quantified invariants for
programs that manipulate singly and doubly linked-list data structures. Our algorithm is …

Induction is a successful approach for verification of hardware and software systems. A
common practice is to model a system using logical formulas, and then use a decision …