Data-Driven Inference of Representation Invariants
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.
Thu 21 OctDisplayed time zone: Central Time (US & Canada) change
15:40 - 17:00 | |||
15:40 15mTalk | A Study of the Learnability of Relational Properties: Model Counting Meets Machine Learning (MCML) SIGPLAN Papers Muhammad Usman University of Texas at Austin, USA, Wenxi Wang University of Texas at Austin, Marko Vasic University of Texas at Austin, USA, Kaiyuan Wang Google, Inc., Haris Vikalo University of Texas at Austin, USA, Sarfraz Khurshid University of Texas at Austin | ||
15:55 15mTalk | Data-Driven Inference of Representation Invariants SIGPLAN Papers Anders Miltner The University of Texas at Austin, Texas, USA, Saswat Padhi Amazon Web Services, USA, Todd Millstein University of California, Los Angeles, David Walker Princeton University, USA | ||
16:10 15mTalk | Reconciling Enumerative and Deductive Program Synthesis SIGPLAN Papers Kangjing Huang Purdue University, USA, Xiaokang Qiu Purdue University, USA, Peiyuan Shen Purdue University, USA, Yanjun Wang Purdue University, USA | ||
16:25 15mTalk | Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations SIGPLAN Papers Chandrakana Nandi Certora, inc., Max Willsey University of Washington, Adam Anderson University of Washington, James R. Wilcox University of Washington, Eva Darulova Uppsala University, Dan Grossman University of Washington, Zachary Tatlock University of Washington | ||
16:40 20mLive Q&A | Discussion, Questions and Answers SIGPLAN Papers | ||