This talk discusses a generalisation of the CDCL algorithm to richer problem domains. The basis of this work is the characterisation of SAT solvers as abstract interpreters in our SAS2012 paper. I gave this talk at Microsoft Research in Redmond in June, you can find a video online here: Abstract Conflict Driven Clause Learning.
This is the presentation for our TACAS2012 paper. It discusses an implementation of a program analyser that uses a clause learning approach for interval analysis.
This talk discusses how SAT solvers can be viewed as abstract interpreters and that various pieces of SAT technology can be understood as specific instantiations of existing program analysis techniques.
A fairly long talk about abstract interpretation and DPLL. Aimed at an abstract interpretation literate audience.
This is a talk aimed at a non-academic audience which attempts to survey work in floating point verification and discusses our work in context. Contains lots of citations to FP verification work.
Brief talk with lots of pictures aimed at a general CS audience.
Very brief talk at the student session of POPL 2011.
Presentation of my VMCAI 2011 paper.
This is the first talk I gave on my abstract interpretation and decision procedures work, right after I started looking at the topic.
Early on in my PhD I did an internship at Microsoft Research with Satnam Singh on building SAT solvers on FPGAs. We have a short paper on this at FMCAD 2010. This is the presentation.