Data-driven inference of representation invariants

Anders Miltner, Saswat Padhi, Todd Millstein, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

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 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.

Original languageEnglish (US)
Title of host publicationPLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsAlastair F. Donaldson, Emina Torlak
PublisherAssociation for Computing Machinery
Pages1-15
Number of pages15
ISBN (Electronic)9781450376136
DOIs
StatePublished - Jun 11 2020
Event41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020 - London, United Kingdom
Duration: Jun 15 2020Jun 20 2020

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020
CountryUnited Kingdom
CityLondon
Period6/15/206/20/20

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Abstract Data Types
  • Logical Relations
  • Type-Directed Synthesis

Fingerprint Dive into the research topics of 'Data-driven inference of representation invariants'. Together they form a unique fingerprint.

  • Cite this

    Miltner, A., Padhi, S., Millstein, T., & Walker, D. (2020). Data-driven inference of representation invariants. In A. F. Donaldson, & E. Torlak (Eds.), PLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 1-15). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)). Association for Computing Machinery. https://doi.org/10.1145/3385412.3385967