Wed 17 Jun 2015 16:25 - 16:50 at PLDI Main BLUE (Portland 254-255) - Synthesis II Chair(s): Isil Dillig

In this paper, we present a technique to synthesize machine-code instructions from a semantic specification, given as a Quantifier-Free Bit-Vector (QFBV) logic formula. Our technique uses an instantiation of the Counter-Example Guided Inductive Synthesis (CEGIS) framework, in combination with search-space pruning heuristics to synthesize instruction-sequences. To counter the exponential cost inherent in enumerative synthesis, our technique uses a divide-and-conquer strategy to break the input QFBV formula into independent sub-formulas, and synthesize instructions for the sub-formulas. Synthesizers created by our technique could be used to create semantics-based binary rewriting tools such as optimizers, partial evaluators, program obfuscators/de-obfuscators, etc. Our experiments for Intel’s IA-32 instruction set show that, in comparison to our baseline algorithm, our search-space pruning heuristics reduce the synthesis time by a factor of 473, and our divide-and-conquer strategy reduces the synthesis time by a further 3 to 5 orders of magnitude.

Wed 17 Jun
Times are displayed in time zone: Tijuana, Baja California change

16:00 - 17:40
Synthesis IIResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Isil DilligUniversity of Texas, Austin
16:00
25m
Talk
Concurrency Debugging with Differential Schedule Projections
Research Papers
Nuno MachadoINESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Brandon LuciaCarnegie Mellon University, Luís RodriguesUniversidade de Lisboa, Instituto Superior Técnico, INESC-ID
Media Attached
16:25
25m
Talk
Synthesis of Machine Code from Semantics
Research Papers
Venkatesh SrinivasanUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.
Media Attached
16:50
25m
Talk
Synthesis of ranking functions using extremal counterexamples
Research Papers
Laure GonnordUniversity of Lyon & LIP, France, David MonniauxCNRS, VERIMAG, Gabriel RadanneUniversité Denis Diderot Paris 7, PPS
Media Attached
17:15
25m
Talk
Type-and-Example-Directed Program Synthesis
Research Papers
Peter-Michael OseraUniversity of Pennsylvania, Steve Zdancewic
Media Attached