Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Wed 2 Nov 2016 13:55 - 14:20 at Matterhorn 2 - Program Synthesis Chair(s): Martin Odersky

Machine-code synthesis is the problem of searching for an instruction sequence that
implements a semantic specification, given as a formula in quantifier-free bit-vector logic (QFBV).
Instruction sets like Intel's IA-32 have around 43,000 unique instruction schemas;
this huge instruction pool, along with the exponential cost inherent in enumerative synthesis,
results in an enormous search space for a machine-code synthesizer: even for
relatively small specifications, the synthesizer might take several hours or days to
find an implementation. In this paper, we present several improvements to the algorithms
used in a state-of-the-art machine-code synthesizer McSynth.
In addition to a novel pruning
heuristic, our improvements incorporate a
number of ideas known from the literature, which we adapt in novel ways for the purpose
of speeding up machine-code synthesis.
Our experiments for Intel's IA-32 instruction set show that our improvements
enable synthesis of code for 12 out of 14 formulas on which McSynth times out,
speeding up the synthesis time by at least 1981X, and for
the remaining formulas, speeds up synthesis by 3X.

Wed 2 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:10
Program SynthesisOOPSLA at Matterhorn 2
Chair(s): Martin Odersky EPFL, Switzerland
13:30
25m
Talk
Deriving Divide-and-Conquer Dynamic Programming Algorithms using Solver-Aided TransformationsAEC
OOPSLA
Shachar Itzhaky MIT CSAIL, Rohit Singh MIT, Rezaul Chowdhury Stony Brook University, Kuat Yessenov MIT, Yongquan Lu MIT, Charles E. Leiserson MIT, Armando Solar-Lezama MIT CSAIL
DOI Pre-print Media Attached
13:55
25m
Talk
Speeding Up Machine-Code Synthesis
OOPSLA
Venkatesh Srinivasan University of Wisconsin - Madison, Tushar Sharma University of Wisconsin - Madison, USA, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
DOI Pre-print Media Attached
14:20
25m
Talk
Automated Reasoning for Web Page LayoutAEC
OOPSLA
Pavel Panchekha University of Washington, Emina Torlak University of Washington
DOI Media Attached
14:45
25m
Talk
FIDEX: Filtering Spreadsheet Data using Examples
OOPSLA
Xinyu Wang UT Austin, Sumit Gulwani Microsoft Research, Rishabh Singh Microsoft Research
DOI Media Attached