2016
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor.
Proceedings of the FM 2016: Formal Methods, 2016

2015
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems.
Proceedings of the 25th Symposium on Operating Systems Principles, 2015

Pattern Matches in HOL: - A New Representation and Improved Code Generation.
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2012
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011
A separation logic framework for HOL.
PhD thesis, 2011

The 1st Verified Software Competition: Experience Report.
Proceedings of the FM 2011: Formal Methods, 2011

2009
A Formalisation of Smallfoot in HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

2006
Model Checking PSL Using HOL and SMV.
Proceedings of the Hardware and Software, 2006

2005
From PSL to LTL: A Formal Validation in HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Maximal Causality Analysis.
Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 2005