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