Menu

School of Electronic Engineering and Computer Science

events menu
Mar 19

Abstract Conflict-Driven Learning

We present a lattice-theoretic generalisation of CDCL, the algorithm behind modern propositional satisfiability solvers, to reasoning in abstract domains. As an exemplar, a bit-precise decision procedure for the theory of floating-point arithmetic is shown. The talk concludes with an overview of further work, presented at POPL 2013 and 2014, and ESOP 2014.This is joint work with Martin Brain, Vijay D’Silva, Alberto Griggio and Leopold Haller.

Abstract


We present a lattice-theoretic generalisation of CDCL, the algorithm behind modern propositional satisfiability solvers, to reasoning in abstract domains. As an exemplar, a bit-precise decision procedure for the theory of floating-point arithmetic is shown. The talk concludes with an overview of further work, presented at POPL 2013 and 2014, and ESOP 2014. This is joint work with Martin Brain, Vijay D’Silva, Alberto Griggio and Leopold Haller.

About the Speaker


Daniel Kroening received the M.E. and doctoral degrees in computer science from the University of Saarland, Saarbrucken, Germany, in 1999 and 2001, respectively. He joined the Model Checking group in the Computer Science Department at Carnegie Mellon University, Pittsburgh PA, USA, in 2001 as a Post-Doc. He was appointed as an assistant professor at the Swiss Technical Institute (ETH) in Zurich, Switzerland, in 2004. In 2007 he joined the University of Oxford and is now a Professor in the Department of Computer Science and a fellow of Magdalen College, Oxford. His research interests include automated formal verification of hardware and software systems, decision procedures, embedded systems, and hardware/software co-design.

Wed 19th March 2014

Start Time: 15:00
End Time: 16:00

 

BR 3.02
Bancroft Road Teaching Rooms
Peter Landin Building
London
E1 4NS

Return to top