BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Abstractions in Satisfiability Solvers - Vijay D'Silva\, Oxford Un
 iversity
DTSTART:20110909T100000Z
DTEND:20110909T110000Z
UID:TALK32688@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Modern satisfiability solvers combine an elegant algorithm wit
 h clever heuristics and efficient engineering to achieve extremely high pe
 rformance. I will show that the Conflict Driven Clause Learning algorithm 
 in modern solvers has a natural characterisation in the framework of abstr
 act interpretation. In particular\, SAT solvers operate on a strict abstra
 ction of propositional logic. This is surprising because an imprecise abst
 raction is used to obtain precise results. Time permitting\, I will discus
 s how one may derive verification algorithms from satisfiability algorithm
 s.\n\nI assume no background in either SAT solving or abstract interpretat
 ion.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR