[pl-seminar] PLDI 2015 Practice Talk

[Venkatesh Srinivasan <venk@xxxxxxxxxxx>]

Hi all,

I will be giving a practice talk for PLDI 2015 at 10 AM on Thursday 
(June 11) in CS 3310. If you are able to attend, I would very much 
appreciate your feedback. Please see the abstract below. The duration of 
the talk is 20 minutes, followed by 5 minutes for questions.
Thanks in advance! I'm not sure if all of you are subscribed to 
pl-seminar, so I apologize if you receive multiple copies of this email.

Title: Synthesis of Machine Code from Semantics
Time: Thursday, June 11 @ 10 AM
Location: CS 3310

Abstract:
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 subformulas. 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.
--
Thanks,
Venkatesh