Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor.
Proceedings of the FM 2016: Formal Methods, 2016
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
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012
A separation logic framework for HOL.
PhD thesis, 2011
The 1st Verified Software Competition: Experience Report.
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
,
Proceedings of the FM 2011: Formal Methods, 2011
A Formalisation of Smallfoot in HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009
Model Checking PSL Using HOL and SMV.
Proceedings of the Hardware and Software, 2006
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