| 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 2004 | Hanne 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 2003 | Joe 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 |
