We introduce ICE, a robust learning paradigm for synthesizing invariants, that learns using
examples, counter-examples, and implications, and show that it admits honest teachers and …

Inductive invariants can be robustly synthesized using a learning model where the teacher is
a program verifier who instructs the learner through concrete program configurations …

We extend the data-driven approach to inferring preconditions for code from a set of test
executions. Prior work requires a fixed set of features, atomic predicates that define the …

Distributed systems are notoriously hard to implement correctly due to non-determinism.
Finding the inductive invariant of the distributed protocol is a critical step in verifying the …

Distributed systems are complex and difficult to build correctly. Formal verification can
provably rule out bugs in such systems, but finding an inductive invariant that implies the …

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 …

Programs with arrays are ubiquitous. Automated reasoning about arrays necessitates
discovering properties about ranges of elements at certain program points. Such properties …

Until recently, model checking and data-flow analysis—two traditional approaches to
software verification—were used independently and in isolation for solving similar problems …

Loops are challenging structures for program analysis, especially when loops contain
multiple paths with complex interleaving executions among these paths. In this paper, we …

Analyzing loops is very important for various software engineering tasks such as bug
detection, test case generation and program optimization. However, loops are very …