Talks

opentheory   •   metis   •   chess   •   talks

2014

• Verifying Relative Error Bounds Using Symbolic Simulation, presented by Alan Hu, CAV 2014, Vienna, Austria.

2013

• Maintaining Verified Software, Haskell Symposium 2013, Boston, Massachusetts, USA.
• Formally Verified Endgame Tables, Guest Lecture, Combinatorial Games, Portland State University, Portland, Oregon, USA.
• Explicit Laziness, Portland Functional Programming Study Group, Portland, Oregon, USA.
• Theory Engineering Using Composable Packages, Invited Talk, SVARM 2013, Rome, Italy.

2012

• FUSE: Inter-Application Security for Android, HCSS 2012, Annapolis, Maryland, USA.
• Cryptol: The Language of Cryptography Cryptanalysis, Invited Talk with Sally Browning, SHARCS 2012, Washington D.C., USA.

2011

• Formally Verified Endgame Tables, Guest Lecture, Combinatorial Games, Portland State University, Portland, Oregon, USA. [blog]
• The OpenTheory Standard Theory Library, NFM 2011, Pasadena, California, USA.
• The OpenTheory Standard Theory Library, Galois Tech Talk, Portland, Oregon, USA. [video]

2010

• Visualizing Information Flow through C Programs, Invited Talk, SSV '10, Vancouver, Canada.
• Treaps, Galois Dev Discussion, Portland, Oregon, USA.
• Visual Mathematics, Ignite Portland 9, Portland, Oregon, USA. [video] [script]
• Random Binary Search Trees, Portland Functional Programming Study Group, Portland, Oregon, USA.
• Portable Higher Order Logic Proofs, presented by Rob Arthan, Workshop on Trusted Extensions of Interactive Theorem Provers, Cambridge, UK.
• Composable Packages for Higher Order Logic Theories, VERIFY 2010, Edinburgh, UK.
• Evaluation Opportunities in Mechanized Theories, Invited Talk, EMS+QMS 2010, Edinburgh, UK.
• Visualizing Information Flow through C Programs, Galois Tech Talk, Portland, Oregon, USA.
• Formal Methods in Use at Galois, Inc, Guest Lecture, Specification & Verification I, Cambridge, UK.
• Packaging Theories of Higher Order Logic, Theory Engineering: Tools and Practice, Cambridge, UK.

2009

• Theory Engineering: Proving in the Large, Workshop on Interactive Theorem Proving, Cambridge, UK.
• OpenTheory: Package Management for Higher Order Logic Theories, PLMMS 2009, Munich, Germany.
• Mathematics of Cryptography: A Guided Tour, Galois Tech Talk, Portland, Oregon, USA.
• Data Assurance in Opaque Computations, presented by Guy Haworth, ACG 2009, Pamplona, Spain.
• OpenTheory: Package Management for Higher Order Logic Theories, Galois Tech Talk, Portland, Oregon, USA.

2008

• Formal Methods in Use at Galois, Inc, Tutorial T-2, IJCAR 2008, Sydney, Australia.
• The Metis Theorem Prover, Intel, Portland, Oregon, USA.
• The Metis Theorem Prover, Galois, Portland, Oregon, USA.

2007

• Proof Pearl: The Termination Analysis of TERMINATOR, TPHOLs 2007, Kaiserslautern, Germany.
• Proof Pearl: The Termination Method of TERMINATOR, CISA Seminar, University of Edinburgh, UK.
• Formally Verified ARM Code, with Anthony Fox, Mike Gordon and Konrad Slind, HCSS 2007, Maryland, USA.
• Formally Verified Elliptic Curve Cryptography, Computer Laboratory, Cambridge, UK.
• Embedding Cryptol in Higher Order Logic, Computer Laboratory, Cambridge, UK.
• Proof Pearl: The Termination Method of TERMINATOR, Galois Connections, Portland, Oregon, USA.
• Formally Verified Elliptic Curve Cryptography for ARM Processors, Department of Computing, Imperial College, London, UK.
• Formally Verified Elliptic Curve Cryptography, ACAC Seminar, Macquarie University, Sydney, Australia.
• Mechanizing the Probabilistic Guarded Command Language, IFIP Working Group 2.3 Meeting 46, Sydney, Australia.

2006

• Mechanizing Elliptic Curve Associativity, Galois Connections, Portland, Oregon, USA.
• Formally Verified ARM Machine Code, Intel, Portland, Oregon, USA.
• Formally Verified Elliptic Curve Cryptography, Åbo Akademi University, Turku, Finland.
• Computer Algebra Systems and Theorem Provers, ARG Lunch, Computer Laboratory, Cambridge, UK.
• Formalized Elliptic Curve Cryptography, with Mike Gordon and Anthony Fox, HCSS 2006, Maryland, USA.

2005

• First Order Proof for Higher Order Logic Theorem Provers, Invited Talk, ESHOL 2005, Montego Bay, Jamaica.
• Metis system description, ESHOL 2005, Montego Bay, Jamaica.
• Formal Verification of Chess Endgame Databases, Poster Session at TPHOLs 2005, Oxford, UK.
• Elliptic Curve Cryptography, Galois Connections, Portland, Oregon, USA.
• Formal Verification of Chess Endgame Databases, ARG Lunch, Computer Laboratory, Cambridge, UK.
• Theorem Proving and Model Checking, Cakes Talk, Computing Laboratory, Oxford, UK.
• Why Computers Go Wrong (And How To Prevent This), Magdalen Research Forum, Magdalen College, Oxford, UK.

2004

• Compiling HOL4 to Native Code, Poster Session, TPHOLs 2004, Park City, Utah, USA.
• Probabilistic Guarded Commands Mechanized in HOL, QAPL 2004, Barcelona, Spain.
• Formal Verification of Probabilistic Programs: Two Approaches, Joint QMUL/Imperial Theory Seminar, Imperial College, London, UK.
• Verification Conditions and Theorem Proving, Guest Lecture, Specification and Verification I, Cambridge, UK.
• Automated Reasoning Methods Used to Prove the Robbins Conjecture, Guest Lecture, Intelligent Systems I, Oxford, UK.

2003

• Assertion Based Verification, Cakes Talk, Computing Laboratory, Oxford, UK.
• Generating Verilog Checkers from PSL Formulas, ARG Lunch, Computer Laboratory, Cambridge, UK.
• First-Order Proof Tactics in Higher Order Logic Theorem Provers, STRATA 2003, Rome, Italy.
• Probabilistic Guarded Commands Mechanized in HOL, Dagstuhl Seminar 03201, Germany.
• Formal Verification of Probabilistic Programs: Two Approaches, Ludwig Maximilians Universität, Munich, Germany.
• Automatic First-Order Proof in HOL, Technische Universität, Munich, Germany.
• Boolification: Encoding High-Level Types as Strings of Bits, ARG Lunch, Computer Laboratory, Cambridge, UK.
• Verifying Probabilistic Programs Using the HOL Theorem Prover, University of New South Wales, Sydney, Australia.

2002

• A Formal Approach to Probabilistic Termination, TPHOLs 2002, Hampton, Virginia, USA.
• A Formal Approach to Probabilistic Termination, University of Utah, Salt Lake City, Utah, USA.
• An LCF-Style Interface between HOL and First-Order Logic, Poster Session, CADE 2002, Copenhagen, Denmark.
• Verifying Multiple Compare and Swap, ARM, Cambridge, UK.
• Formalizing a CAS(n) Algorithm in HOL (and a simulation trace of RDCSS with 3 processors), ARG Lunch, Computer Laboratory, Cambridge, UK.
• HOL Theorem Prover Case Study: Verifying Probabilistic Programs, AVoCS 2002, Birmingham, UK.
• Fast Normalization in the HOL Theorem Prover, ARW 2002, Imperial College, London, UK.
• The Schroeder-Bernstein Theorem, Guest Lecture, Discrete Mathematics, Cambridge, UK.
• Verifying Probabilistic Programs Using the HOL Theorem Prover, Logic Summer School, ANU, Canberra, Australia.

2001

• Verifying Probabilistic Programs Using the HOL Theorem Prover, University of Birmingham, UK.
• Predicate Subtypes with Predicate Sets, TPHOLs 2001, Edinburgh, UK.
• Verification of the Miller-Rabin Probabilistic Primality Test, Poster Session, TPHOLs 2001, Edinburgh, UK.
• Verification of the Miller-Rabin Probabilistic Primality Test, University of Edinburgh, UK.
• Verification of the Miller-Rabin Probabilistic Primality Test, University of Sheffield, UK.
• Bisimulation Games, Game Theory Study Group, Computer Laboratory, Cambridge, UK.

2000

• Predicate Subtyping in HOL, ARG Lunch, Computer Laboratory, Cambridge, UK.
• Congruence Classes with Logic Variables, Poster Session, TPHOLs 2000, Portland, Oregon, USA.
• Lightweight Probability Theory for Verification, Poster Session, TPHOLs 2000, Portland, Oregon, USA.
• Congruence Classes with Logic Variables (and extra results slides), ARW 2000, Kings College, London, UK.
• Equality Reasoning and Logical Proving, ARG Lunch, Computer Laboratory, Cambridge, UK.
• Viewing Proofs (and the example html proof of `prime 2`), ARG Lunch, Computer Laboratory, Cambridge, UK.

1999

• Integrating Gandalf and HOL, TPHOLs 1999, Nice, France.

1997

• Blum Integers, Trinity Mathematical Society, Cambridge, UK.