Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Wed 17 Jun 2020 08:00 - 08:20 at PLDI Research Papers live stream - Synthesis I Chair(s): James Bornholt

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.

Wed 17 Jun
Times are displayed in time zone: Pacific Time (US & Canada) change

08:00 - 09:00: Synthesis IPLDI Research Papers at PLDI Research Papers live stream
Chair(s): James BornholtUniversity of Texas at Austin

YouTube lightning session video

08:00 - 08:20
Data-Driven Inference of Representation Invariants
PLDI Research Papers
Anders MiltnerPrinceton University, USA, Saswat PadhiUniversity of California at Los Angeles, USA, Todd MillsteinUniversity of California at Los Angeles, USA, David WalkerPrinceton University, USA
08:20 - 08:40
Type Error Feedback via Analytic Program Repair
PLDI Research Papers
Georgios SakkasUniversity of California at San Diego, USA, Madeline EndresUniversity of Michigan, USA, Benjamin CosmanUniversity of California at San Diego, USA, Westley WeimerUniversity of Michigan, USA, Ranjit JhalaUniversity of California at San Diego, USA
08:40 - 09:00
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
PLDI Research Papers
Chandrakana NandiUniversity of Washington, USA, Max WillseyUniversity of Washington, USA, Adam AndersonUniversity of Washington, USA, James R. WilcoxCertora, USA, Eva DarulovaMPI-SWS, Germany, Dan GrossmanUniversity of Washington, USA, Zachary TatlockUniversity of Washington, Seattle