Automated Reasoning Group
Most of the links in this page are dead. TODO cleanup.

Past lunches

Here are details of some past talks:

Date Event
Tue 18 Sep 2007 Domagoj Babic, University of British Columbia: Boosting Verification by Automatic Tuning of Decision Procedures
Tue 14 Aug 2007 Mateusz Srebrny: Cryptanalysis with SAT - a propositional programming environment
Tue 07 Aug 2007 Rajeev Goré: One-pass Tableaux for Computation Tree Logic
Tue 03 Jul 2007 Christoph Benzmueller: Progress Report on Leo-II, an Automatic Theorem Prover for Higher-Order Logic
Tue 26 Jun 2007 Thomas Tuerk: A Deep Embedding of a Decidable Fragment of Separation Logic in HOL
Tue 19 Jun 2007 Nathan Chong and Samin Ishtiaq, ARM: The ARM Cortex-M1 Architecture in Coq
Tue 12 Jun 2007 Roger Bishop Jones: From QED to X-Logic, following the lead of Leibniz
Tue 05 Jun 2007 Aaron Coble: Connecting Partial and Total Correctness for Probabilistic Programs in HOL4
Tue 29 May 2007 Hasan Amjad: A Compressing Translation from Propositional Resolution to Natural Deduction
Tue 15 May 2007 Alexey Gotsman, ARG: Local Reasoning for Storable Locks and Threads
Tue 08 May 2007 Ozan Kahramanoğullari, Imperial College London: Deep Inference in Theorem Proving
Tue 6 Mar 2007 Hasan Amjad, ARG: Compressing Propositional Refutations using Subsumption
Tue 27 Feb 2007 Larry Paulson, ARG: Extending Resolution to Prove Inequalities On Elementary Functions
Tue 20 Feb 2007 Tom Melham, Oxford University Computing Laboratory: Practical Formal Verification at an Industrial Scale
Tue 13 Feb 2007 Tom Ridge, TSG: Operational reasoning for real languages with concurrency: Peterson's mutual exclusion algorithm in OCaml
Tue 6 Feb 2007 Satnam Singh, MSR Cambridge: Quicker Unsatisfaction
Tue 30 Jan 2007 Viktor Vafeiadis, CPRG: Automatic safety checking for fine-grain concurrency
Tue 23 Jan 2007 Christoph Benzmueller, ARG: Challenges for Automated Theorem Proving in Classical Higher-Order Logic
Tue 12 Dec 2006 Aaron Coble, ARG: Analyzing the Dining Cryptographers using the probabilistic Guarded Command Language (pGCL) formalized in the HOL4 theorem prover
Tue 5 Dec 2006 Joe Hurd, ARG: Formally Verified ARM Machine Code Implementing Elliptic Curve Cryptography
Tue 28 Nov 2006 Byron Cook, MSR Cambridge: Title: (Secret)
Tue 21 Nov 2006 Larry Paulson, ARG: Integrating Interactive and Automatic Theorem Provers: Some Results
Tue 14 Nov 2006 Lee Pike, Galois Connections, Inc.: A Verifying Core for a Cryptographic Language Compiler
Tue 7 Nov 2006 Thomas Tuerk, ARG: A verifying ARM compiler in HOL
Tue 31 Oct 2006 Tom Ridge, TSG: Rigorous protocol design in practice: an optical packet-switch MAC in HOL
Tue 24 Oct 2006 Magnus Myreen, ARG: Hoare Logic for Realistically Modelled Machine Code
Tue 12 Sep 2006 Judit Robu, Babes-Bolyai University of Cluj, Automated Geometry Theorem Proving in the Frame of the Theorema Project
Tue 5 Sep 2006 John Lloyd, Computer Sciences Laboratory, the Australian National University: Knowledge Representation and Reasoning in Modal Higher-order Logic
Tue 18 July 2006 Byron Cook, MSR Cambridge: Termination Analyses for Free!
Wed 5 July 2006 Joe Hurd, ARG: Computer Algebra Systems and Theorem Provers
Wed 28 June 2006 Kristin Yvonne Rozier: Algorithms for Automata-Theoretic Linear Temporal Logic Model Checking
Wed 21 June 2006 Thomas Tuerk, ARG: Deep Embeddings of Temporal Logics in HOL
Wed 14 June 2006 David Greaves, SRG: Formal Checking and Synthesis of Controller Nodes
Wed 31 May 2006 Peter Sewell, TSG: Ott2: Tool Support for the Working Semanticist
Wed 24 May 2006 Behzad Akbarpour, ARG: Towards Automatic Proofs of Inequalities Involving Elementary Functions
Wed 17 May 2006 Alexey Gotsman, ARG: Interprocedural Shape Analysis with Separation Logic
Wed 10 May 2006 Larry Paulson, ARG: Computational Logic and the Quest for Greater Automation
Wed 29 March 2006 Kathi Fisler: Temporal Modalities for Concisely Capturing Timing Diagrams (joint work with Hana Chockler)
Wed 22 March 2006 Joe Hurd, ARG: Formalized Elliptic Curve Cryptography
Wed 15 March 2006 James Reynolds, ARG: Translating HOL4 definitions to ACL2: Process Overview
Wed 8 March 2006 Kong Woei Susanto, ARG: Verification Platform for System on Chip
Wed 22 February 2006 Alexey Gotsman, ARG: Practical Program Analysis for Liveness and Fairness
Wed 15 February 2006 Behzad Akbarpour, ARG: Modeling and Verification of DSP Designs in HOL
Wed 8 February 2006 Magnus Myreen, ARG: Tool Support for Invariant Based Programming
Wed 1 February 2006 Thomas Türk, ARG: PSL in HolCheck
Thu 26 January 2006 Moshe Vardi at Microsoft Research: The Design of a Formal Property-Specification Language
Wed 30 November 2005 Larry Paulson, ARG: Integrating Isabelle with Automatic Theorem Provers: Experiments and Outcomes
Wed 23 November 2005 Michael Compton, ARG: Simple Compositional Proofs for Process Algebras
Wed 9 November 2005 Tom Ridge, TSG: Craig's Interpolation Theorem
Wed 2 November 2005 Mateja Jamnik, ARG: Can Machines Reason like Humans in Mathematics?
Wed 26 October 2005 Hasan Amjad, ARG: Fast Propositional Tautology Checking in HOL
Wed 19 October 2005 Mike Gordon, ARG: Linking HOL4 and ACL2: Purpose, Progress, Plans
Wed 6 July 2005 Michael Compton, ARG: A fair CCS in Isabelle/Hol
Wed 22 June 2005 Larry Paulson, ARG: Integrating Isabelle with Automatic Theorem Provers: Status and Prospects
Wed 15 June 2005 Andrey Rybalchenko, Max-Planck-Institut fr Informatik: Constrained Linear Interpolation
Wed 8 June 2005 Joe Hurd, Oxford University Computing Laboratory: Formal Verification of Chess Endgame Databases
Wed 1 June 2005 Juliano Iyoda, ARG: Proof-producing Hardware Compiler for a Subset of HOL
Wed 11 May 2005 Ursula Martin, ARG: Reasoning about linear systems
Wed 4 May 2005 Gem Stapleton, University of Brighton: Reasoning with Diagrams
Wed 30 March 2005 Hasan Amjad, ARG: Shallow Lazy Proofs
Wed 23 March 2005 Georges Gonthier, Microsoft Research: Verifying the Four Colour Theorem
Wed 16 March 2005 Byron Cook, Microsoft Research: Counterexample-Guided Abstraction Refinement for Termination
Wed 2 March 2005 Larry Paulson, ARG: Monads in Verification: Research Directions
Wed 16 February 2005 Claire Quigley, ARG: Watching Vampires - the story so far
Wed 9 February 2005 Anthony Fox, ARG: Formal Verification of Microprocessors: Input and Output
Wed 8 December 2004 Byron Cook, Microsoft Research: Automatic theorem proving for software model checking
Wed 1 December 2004 Larry Paulson, ARG: The World's Slowest Model-Elimination Theorem Prover
Wed 17 November 2004 Mike Gordon, ARG: Overview of new projects and vague plans
Wed 3 November 2004 Juliano Iyoda, ARG: Higher-Level Hardware Synthesis in HOL
Wed 27 October 2004 Michael Compton, ARG: Stenning's Protocol: Implemented using UDP and verified in Isabelle
Wed 20 October 2004 Christoph Benzmueller and Martin Pollet: OMEGA: An Attempt to build a Mathematics Assistance System
Wed 15 September 2004 Christian Urban: Nominal Techniques as an Isabelle/HOL-Theory
Wed 14 July 2004 Anthony Fox, ARG: Formal Verification of ARM6 Exceptions
Wed 30 June 2004 Jia Meng, ARG: Supporting Interactive Proof Using Resolution
Wed 23 June 2004 Larry Paulson, ARG: Formalizing Abstract Mathematics: Issues and Progress
Wed 16 June 2004 Hasan Amjad, ARG: Using HOL Within the Model Checking Workflow
Wed 19 May 2004 Larry Paulson, ARG: Defining Functions on Equivalence Classes
Mon 10 May 2004 Kathi Fisler: Drawing on Dimensions: The Unique Logic of Timing Diagrams (This talk will be the same as Semantics Lunch)
Wed 25 February 2004Hanne Gottliebsen, Queen Mary University of London: Formal Methods for SATS HVO
Wed 18 February 2004 Larry Paulson, ARG: Organizing Numerical Theories using Axiomatic Type Classes
Tue 2 December 2003 Lucas Dixon, University of Edinburgh: On Proof planning in Isabelle
Tue 25 November 2003 Hasan Amjad, ARG: Towards Model Checking AMBA
Tue 18 November 2003 Anthony Fox, ARG: Verifying ARM6 Multiplication
Tue 4 November 2003Joe Hurd, ARG: Generating Verilog checkers from PSL formulas
Tue 21 October 2003 Larry Paulson, ARG: Seven Years of Verifying Security Protocols
Tue 14 October 2003 Mike Gordon, ARG: Can theorem proving ever be useful?
Tue 2 September 2003 Anthony Fox, ARG: Formal Specification and Verification of the ARM6
Tue 8 July 2003 Jia Meng, ARG: Integrating Isabelle and Vampire
Tue 1 July 2003 Mike Gordon, ARG: Verification by theorem proving: issues and challenges
Tue 24 June 2003 Michael Compton, ARG: A timed temporal logic in Isabelle/HOL
Tue 17 June 2003 Richard Sharp, Intel: Higher-Level Hardware Synthesis
Tue 3 June 2003 Hasan Amjad, ARG: Implementing abstraction for model checking in HOL
Tue 27 May 2003 Eli Katsiri, LCE: Knowledge-Representation and Scalable Abstract Reasoning for Sentient Computing using First-Order Logic
Tue 13 May 2003 Mike Gordon, ARG: Executing the formal semantics of the Accellera Property Specification Language
Tue 29 April 2003 Joe Hurd, ARG: Probabilistic Guarded Commands Mechanized in HOL
Tue 18 March 2003 Juliano Iyoda, ARG: Algebraic Synthesis and its Healthiness Verification with HOL
Tue 11 March 2003 Mike Gordon, ARG: Is the Time Ripe for Another Attempt to Merge Computation and Deduction?
Tue 4 March 2003 Joe Hurd, ARG: Boolification: Encoding High-Level Types as Strings of Bits
Tue 25 February 2003 Anthony Fox, ARG: Verifying ARM's Block Data Transfer Instructions
Tue 18 February 2003 Peter Sewell, NetSem Project, Theory and Semantics Group: TCP Failure Semantics - Segment-Level Specification
Tue 17 December 2002 Graham Steel, Edinburgh University: Discovering Security Protocol Attacks by Refuting Incorrect Conjectures
Tue 3 December 2002 Anthony Fox, ARG: Temporal Abstraction for Memory Stalls
Tue 26 November 2002 Larry Paulson, ARG: The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF
Tue 19 November 2002 Joe Hurd, ARG: Automatic First-Order Proof in HOL
Tue 12 November 2002 Michael Norrish, ARG: Mechanising lambda-calculus proofs with the Gordon-Melham axioms for bound names
Tue 5 November 2002 Mike Gordon, ARG: Sugar and HOL
Tue 29 October 2002 Hasan Amjad, ARG: BDD-based mu-Calculus Model Checking in HOL
Tue 22 October 2002 William Stoye, Tenison EDA: A Verilog to C translator.
Tue 18 June 2002 Ernie Cohen, Microsoft Research, Cambridge: First-order verification of crypto protocols
Thu 13 June 2002 Don Syme, Microsoft Research, Cambridge: Automating Type Soundness Proofs via Decision Procedures and Guided Reductions
Thu 6 June 2002 Predrag Janicic, University of Belgrade, Yugoslavia: A General Setting for the Flexible Combining and Augmenting of Decision Procedures
Tue 28 May 2002 Marino Miculan, University of Udine, Italy: The Theory of Contexts: an axiomatic approach to metareasoning on HOAS specifications in Higher Order Logics
Tue 21 May 2002 Mike Gordon, Anthony Fox, and Joe Hurd: A selection of talks relating to the ARM project.
Tue 14 May 2002 Mateja Jamnik: Automatic Learning of Proof Methods in Proof Planning
Tue 7 May 2002 Joe Hurd: Formalizing a CAS(n) algorithm in HOL
Tue 26 March 2002 Michael Norrish: Implementing the Omega Test in HOL
Tue 19 March 2002 Daryl Stewart: Model Checking HDL Simulation
Tue 5 March 2002 Ashish Darbari, University of Glasgow: A Tutorial Talk on Symbolic Trajectory Evaluation
Tue 12 February 2002 Anthony Fox: ARM6 Verification, Part II
Tue 5 February 2002 Anthony Fox: ARM6 Verification, Part I
Tue 29 January 2002 Mike Gordon: HolSatLib and HolBddLib.
Tue 18 December 2001 Konrad Slind, University of Utah: Formalizing the Rijndael block cipher.
Tue 29 May 2001 Ken Friis Larsen, IT University of Copenhagen: Red-Black trees: A tutorial on how to construct them and how to prove properties about them
Wed 16 May 2001 Joe Hurd: Verification of the Miller-Rabin Probabilistic Primality Test
Tue 15 May 2001 Joakim von Wright, Abo Akademi University: Action contracts, game tree logic, and zig-zag-simulation
Tue 8 May 2001 Hassen Saidi, SRI: The combination of abstraction and state exploration techniques
Tue 1 May 2001 Larry Paulson: SET Cardholder Registration: the Secrecy Proofs
Tue 7 November 2000 Peter Sewell: Informal Proof Assistants
Tue 31 October 2000 Daryl Stewart: Model Checking and Compositional Reasoning
Tue 24 October 2000 Joe Hurd: Predicate Subtyping in HOL
Tue 26 September 2000 Conor McBride: Linear Contexts in Regular Datatypes
Wed 9 August 2000 Silvio Ranise: A Practical Extension Mechanism for Decision Procedures
Tue 8 August 2000 Silvio Ranise: Constraint Contextual Rewriting
Tue 18 July 2000 Joe Hurd: 2 Short Talks: Congruence Closure & Probability
Tue 23 May 2000 Michael Norrish: Cooper's algorithm as a derived rule in HOL
Tue 29 February 2000 Joe Hurd: Attempts to Bridge the Gap between Equality Reasoning and Logical Proving
Tue 22 February 2000 Daryl Stewart: Modular Model Checking of Self-Timed Systems
Tue 1 February 2000 Tanja Vos: UNITY in diversity: a stratified approach towards the verification of distributed algorithms.
Tue 25 January 2000 Joe Hurd: Viewing Proofs
Tue 11 January 2000 Thomas Rasmussen: Signed Interval Logic
Tue 9 November 1999 Konrad Slind: Survey of higher-order recursive function definition packages.
Tue 26 October 1999 Mark Staples: Linking ACL2 and HOL
Tue 19 October 1999 Jamie Gabbay: Syntax modulo alpha conversion in Isabelle: First, build a set theory...
Tue 7 September 1999 Joe Hurd: Integrating Gandalf and HOL
Mark Staples: Representing WP Semantics in Isabelle/ZF
Tue 3 August 1999 Paul Curzon: Including the User in Formal System Verification
  Long-term projects

Lab Publications
Technical Reports
Last modified on Wed May 9 23:10:47 BST 2012 by ns441 | Privacy policy