| 13 April 2018 |
ARW 2018 |
Real-world formal documentation (slides, abstract) |
| 24 Aug. 2015 |
ITP 2015 |
Pattern Matches in HOL: A New Representation and Improved Code Generation (slides) |
| 13 Aug. 2012 |
ITP 2012 |
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm (slides) |
| 29 Feb. 2012 |
Club2 |
A Formalisation of Finite Automata in Isabelle/HOL (slides, printer version) |
| 1 Feb. 2011 |
ARG Lunch |
Quantifier Heurististics in HOL4 (slides, printer version) |
| 18 Aug. 2010 |
VSTTE'10 - Theory Workshop |
Local Reasoning about While-Loops (slides, paper) |
| 26 Jan. 2010 |
ARG Lunch |
A demo of Holfoot (slides, printer version) |
| 24 Nov. 2009 |
ARG Lunch |
A presentation of some tools used for Holfoot (slides, printer version) |
| 19 Aug. 2009 |
TPHOLs |
A formalisation of Smallfoot in HOL (slides, printer version) |
| 5 May 2009 |
ARG Lunch |
A Heap of Problems (slides, printer version) |
| 27 Jan. 2009 |
ARG Lunch |
A HOL implementation of Smallfoot (slides, printer version) |
| 2 Sep. 2008 |
Research & review meeting |
A fully-expansive HOL implementation of Smallfoot (slides, printer version) |
| 19 Feb. 2008 |
ARG Lunch |
An Embedding of Abstract Separation Logic in HOL (slides, printer version) |
| 26 Jun. 2007 |
ARG Lunch |
A Deep Embedding of a Decidable Fragment of Separation Logic in HOL (slides, detailed documentation) |
| 7 Nov. 2006 |
ARG Lunch |
A verifying ARM compiler (slides, printer version) |
| 23 Oct. 2006 |
Haifa Verification Conference |
Model Checking PSL using HOL and SMV (slides, printer version) |
| 21 Jun. 2006 |
ARG Lunch |
Deep Embeddings of Temporal Logics in HOL (slides, printer version) |
| 1 Feb. 2006 |
ARG Lunch |
PSL in HolCheck (slides, printer version) |
| 23 Aug. 2005 |
TPHOLs |
From PSL to LTL: A Formal Validation in HOL (slides, printer version) |
