Time: 3:00 - 4:00pm Venue: BR 3.02 Bancroft Road Teaching Rooms Peter Landin Building London E1 4NS
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.
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.