BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:&quot\;... and then just encode it to SAT.&quot\; - Martin Brain\,
  University of Oxford
DTSTART:20150424T090000Z
DTEND:20150424T100000Z
UID:TALK59283@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Encoding problems to Boolean satisfiability is a common techni
 que in state-of-the-art program verification tools and theorem provers.  E
 very problem can be encoded in many different ways and the choice of encod
 ing can have a major effect on performance.\nUnfortunately there are few t
 ools\, theoretical or practical\, to compare encodings or design better on
 es.  This talk introduces an ongoing program of work which will address th
 is problem.  We show how the language of abstract interpretation can be us
 ed to capture the notion of the propagating power of an encoding and how t
 his can be used to automatically generate optimal encodings.  This not onl
 y improves solver performance but also gives a language to explore problem
  difficulty and understand encodings.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR