Papers

• Refereed Papers
  1. Towards Automatic Stability Analysis For Rely-Guarantee Proofs (with Richard Bornat). Conference on Verification, Model Checking and Abstract Interpretation. 2009. PDF
  2. Inter-process Buffers in Separation Logic with Rely/Guarantee (with Richard Bornat). Formal Aspects of Computing. (In review)
  3. Model Checking for Stability Analysis in Rely-Guarantee Proofs (with Richard Bornat). Verification Workshop. 2008. PDF
  4. Data Compression for Proof Replay. Formal Aspects of Computing. 2008. PDF
  5. LCF-style Propositional Simplification with SAT solvers and BDDs. Conference on Theorem Proving in Higher-Order Logics. 2008. PDF [11]
  6. A Compressing Translation from Propositional Resolution to Natural Deduction. Conference on Frontiers of Combining Systems. 2007. PDF [10]
  7. Efficiently Checking Propositional Refutations in HOL Theorem Provers (with Tjark Weber). Journal of Applied Logic. 2007. PDF [13]
  8. Compressing Propositional Refutations. AVoCS 2006. PDF [9]
  9. Shallow Lazy Proofs. TPHOLs 2005. PDF [7]
  10. Verification of AMBA Using a Combination of Model Checking and Theorem Proving. AVoCS 2005. PDF [8]
  11. Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. TPHOLs 2003. PDF [4]
• Unrefereed or short papers
  1. Formalising the Translation of CTL to . TPHOLs 2003. PDF [2]
  2. Implementing Abstraction Refinement for Model Checking in HOL. TPHOLs 2003. PDF [3]
  3. BDD representation judgements in HOL. TPHOLs 2001. PDF [1]
• Technical reports
  1. Combining model checking and theorem proving. PhD thesis. Cambridge University, 2004. PDF [5]
  2. Model checking the AMBA protocol in HOL. Cambridge University, 2004. PDF [6]
• Unpublished
  1. A Process Algebra Model of Classical Multiplicative Linear Logic. MSc short dissertation. Oxford University, 1999. PS