Using Term Rewriting to Solve Bit-Vector Arithmetic Problems - (Poster Presentation).
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012
Standalone Tactics Using OpenTheory.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012
The OpenTheory Standard Theory Library.
Proceedings of the NASA Formal Methods, 2011
Evaluation Opportunities in Mechanized Theories.
Proceedings of the Workshop on Evaluation Methods for Solvers, 2010
Composable Packages for Higher Order Logic Theories.
Proceedings of the 6th International Verification Workshop, 2010
Computer Assisted Reasoning.
J. Autom. Reason., 2009
Data Assurance in Opaque Computations.
Proceedings of the Advances in Computer Games, 12th International Conference, 2009
Proof Pearl: The Termination Analysis of Terminator.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007
Probabilistic guarded commands mechanized in <i>HOL</i>.
Theor. Comput. Sci., 2005
Functional Correctness Proofs of Encryption Algorithms.
Proceedings of the Logic for Programming, 2005
Verification of the Miller-Rabin probabilistic primality test.
J. Log. Algebraic Methods Program., 2003
Applications of Polytypism in Theorem Proving.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving.
Proceedings of the Correct Hardware Design and Verification Methods, 2003
A Formal Approach to Probabilistic Termination.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002
An LCF-Style Interface between HOL and First-Order Logic.
Proceedings of the Automated Deduction, 2002
Congruence Classes with Logic Variables.
Log. J. IGPL, 2001
Predicate Subtyping with Predicate Sets.
Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001
Integrating Gandalf and HOL.
Proceedings of the Theorem Proving in Higher Order Logics, 12th International Conference, 1999