Data-Driven Inference of Representation Invariants
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020), June 15-20, 2020.
Distinguished Paper Award
Anders Miltner, Saswat Padhi, Todd Millstein, David Walker
A representation invariant is a property
that holds of all values of abstract type produced by a
module. Representation invariants play important roles in software
engineering and program verification. In this paper, we develop a
counterexample-driven algorithm for inferring a representation
invariant that is sufficient to imply a desired specification for
a module. The key novelty is a type-directed notion of visible
inductiveness, which ensures that the algorithm makes progress
toward its goal as it alternates between weakening and
strengthening candidate invariants. The algorithm is parameterized
by an example-based synthesis engine and a verifier, and we prove
that it is sound and complete for first-order modules over finite
types, assuming that the synthesizer and verifier are as well. We
implement these ideas in a tool called Hanoi, which synthesizes
representation invariants for recursive data types. Hanoi not only
handles invariants for first-order code, but higher-order code as
well. In its back end, Hanoi uses an enumerative synthesizer
called Myth and an enumerative testing tool as a verifier. Because
Hanoi uses testing for verification, it is not sound, though our
empirical evaluation shows that it is successful on the benchmarks
we investigated.
[PDF]