BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Solving Second-Order Constraints with Program Synthesis - Cristina
  David\, Oxford University
DTSTART:20150714T100000Z
DTEND:20150714T104500Z
UID:TALK60130@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In this talk I'll summarise my work on expressing and solving 
 program analysis problems as second-order satisfiability with an emphasis 
 on the solving part. I'll start by introducing a decidable fragment of sec
 ond-order logic that is expressive enough to capture numerous program anal
 ysis problems (e.g. safety proving\, bug finding\, termination and non-ter
 mination proving\, superoptimisation\, complexity analysis). Subsequently\
 , I will describe the solver we have built for this fragment\, which is ba
 sed on program synthesis. In particular\, we rely on the synthesis of fini
 te state programs\, which we showed to be NEXPTIME-complete. Our synthesis
 er is an instance of the Counterexample Guided Inductive Synthesis (CEGIS)
  framework and can be used to synthesise C programs from a specification w
 ritten in a subset of C. For this purpose it makes use of explicit proof s
 earch\, symbolic bounded model checking and genetic programming. I'll conc
 lude with some experimental results.
LOCATION:Small lecture room\, Microsoft Research Ltd\, 21 Station Road\, C
 ambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR