Data-Driven Inference of Representation Invariants

Anders Miltner,  Saswat PadhiTodd MillsteinDavid Walker

Proceedings of the 41 st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020
⟨ PLDI 2020 ⟩

  PDF
  Tool
Abstract

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 conditional 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 our algorithm, explain how to extend it to handle higher-order code, and evaluate its effectiveness on a range of modules that implement common data structures using recursive data types.

BibTeX Citation
@inproceedings{pldi20/miltner/hanoi,
  title     = {Data-Driven Inference of Representation Invariants},
  author    = {Anders Miltner and
               Saswat Padhi and
               Todd D. Millstein and
               David Walker},
  booktitle = {Proceedings of the 41st {ACM} {SIGPLAN} Conference on Programming
               Language Design and Implementation, {PLDI} 2020, London, UK,
               June 15-20, 2020},
  publisher = {ACM},
  year      = {2020},
  note      = {To appear}
}