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: Tijuana, Baja California change
14:00 - 15:30 | |||
14:00 20mTalk | 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 | ||
14:20 20mTalk | Using Active Learning to Synthesize Models of Applications That Access Databases PLDI Research Papers DOI Media Attached | ||
14:40 20mTalk | 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 | ||
15:00 20mTalk | 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 |