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.

Mon 24 Jun
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

14:00 - 15:30: PLDI Research Papers - Synthesis at 229AB
Chair(s): Nuno P. LopesMicrosoft Research
pldi-2019-papers14:00 - 14:20
Tristan KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
Media Attached
pldi-2019-papers14:20 - 14:40
Jiasi ShenMassachusetts Institute of Technology, Martin RinardMassachusetts Institute of Technology
DOI Media Attached
pldi-2019-papers14:40 - 15:00
Yuepeng WangUniversity of Texas at Austin, James DongUniversity of Texas at Austin, USA, Rushi ShahUT Austin, Isil DilligUT Austin
Media Attached
pldi-2019-papers15:00 - 15:20
Arun IyerMicrosoft Research, India, Manohar JonnalageddaInpher Inc., Switzerland, Suresh ParthasarathyMicrosoft Research, India, Arjun RadhakrishnaMicrosoft, Sriram RajamaniMicrosoft Research
Media Attached