Mon 24 Jun 2019 14:00 - 14:20 at 229AB - Synthesis Chair(s): Nuno P. Lopes

This article presents resource-guided synthesis, a technique
for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that
combines polymorphic refinement types with potential annotations of automatic amortized resource analysis. The type
system enables efficient constraint-based type checking and
can express precise refinement-based resource bounds. The
proof of type soundness shows that synthesized programs
are correct by construction. By tightly integrating program
exploration and type checking, the synthesizer can leverage
the user-provided resource bound to guide the search, eagerly rejecting incomplete programs that consume too many
resources. An implementation in the resource-guided synthesizer ReSyn is used to evaluate the technique on a range of recursive data structure manipulations. The experiments show
that ReSyn synthesizes programs that are asymptotically
more efficient than those generated by a resource-agnostic
synthesizer. Moreover, synthesis with ReSyn is faster than a
naive combination of synthesis and resource analysis. ReSyn
is also able to generate implementations that have a constant
resource consumption for fixed input sizes, which can be used
to mitigate side-channel attacks.

Conference Day
Mon 24 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
SynthesisPLDI Research Papers at 229AB
Chair(s): Nuno P. LopesMicrosoft Research
Resource-Guided Program Synthesis
PLDI Research Papers
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
Media Attached
Using Active Learning to Synthesize Models of Applications That Access Databases
PLDI Research Papers
Jiasi ShenMassachusetts Institute of Technology, Martin C. RinardMassachusetts Institute of Technology
DOI Media Attached
Synthesizing Database Programs for Schema Refactoring
PLDI Research Papers
Yuepeng WangUniversity of Texas at Austin, James DongUniversity of Texas at Austin, USA, Rushi ShahUT Austin, Isil DilligUT Austin
Media Attached
Synthesis and Machine Learning for Heterogeneous Extraction
PLDI Research Papers
Arun IyerMicrosoft Research, India, Manohar JonnalageddaInpher Inc., Switzerland, Suresh ParthasarathyMicrosoft Research, India, Arjun RadhakrishnaMicrosoft, Sriram RajamaniMicrosoft Research
Media Attached