Re: [pl-seminar] ROOM CHANGE - PLDI 2015 Practice Talk

[Venkatesh Karthik Srinivasan <venk@xxxxxxxxxxx>]

Hi all,

Unfortunately, I had issues with the projector in 3310.
I will give the talk in 4310 CS at 10 AM. Please note the change in 
room.
Sorry for the inconvenience!

On 2015-06-09 14:59, Venkatesh Srinivasan wrote:
> 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