| Publication | Date of Publication | Type |
|---|
| Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading | 2025-08-19 | Paper |
| Hammering Floating-Point Arithmetic | 2024-05-03 | Paper |
Weak nominal modal logic
Formal Techniques for Distributed Objects, Components, and Systems | 2022-06-15 | Paper |
| Proof-theoretic conservative extension of HOL with ad-hoc overloading | 2021-07-08 | Paper |
Modal logics for nominal transition systems
(available as arXiv preprint) | 2021-03-26 | Paper |
| Modal logics for nominal transition systems | 2021-03-26 | Paper |
| Model-theoretic conservative extension for definitional theories | 2019-11-12 | Paper |
| Modal logics for nominal transition systems | 2017-09-12 | Paper |
The largest respectful function
Logical Methods in Computer Science | 2016-07-06 | Paper |
Psi-calculi in Isabelle
Journal of Automated Reasoning | 2016-05-26 | Paper |
The 2013 evaluation of SMT-COMP and SMT-LIB
Journal of Automated Reasoning | 2016-05-26 | Paper |
Programming and automating mathematics in the Tarski-Kleene hierarchy
Journal of Logical and Algebraic Methods in Programming | 2014-09-08 | Paper |
Mathematizing C++ concurrency
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
| Integrating a SAT solver with an LCF-style theorem prover | 2013-09-26 | Paper |
| Bounded model generation for Isabelle/HOL | 2013-09-25 | Paper |
Program analysis and verification based on Kleene algebra in Isabelle/HOL
Interactive Theorem Proving | 2013-08-07 | Paper |
Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
Certified Programs and Proofs | 2011-11-22 | Paper |
Validating QBF Validity in HOL4
Interactive Theorem Proving | 2011-08-17 | Paper |
Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
Relational and Algebraic Methods in Computer Science | 2011-06-17 | Paper |
Fast LCF-Style Proof Reconstruction for Z3
Interactive Theorem Proving | 2010-09-14 | Paper |
Validating QBF invalidity in HOL4
Interactive Theorem Proving | 2010-09-14 | Paper |
| On commutativity and groupoid identities between products with 3 factors. | 2009-10-23 | Paper |
Finite Models in FOL-Based Crypto-Protocol Verification
Foundations and Applications of Security Analysis | 2009-10-22 | Paper |
Formal memory models for the verification of low-level operating-system code
Journal of Automated Reasoning | 2009-08-31 | Paper |
Efficiently checking propositional refutations in HOL theorem provers
Journal of Applied Logic | 2009-03-25 | Paper |
Towards Automated Proof Support for Probabilistic Distributed Systems
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2005-08-22 | Paper |
