Logic programming beyond Prolog

This is a MSR Seminar (Station Road), duplicated on the ARG list

Maarten van Emden ( University of Victoria, Canada).

Seminar Room, Microsoft Research, Station Road, Cambridge.

Thursday 09 October 2014, 14:00-15:00

Interfacing and improving proof tools

Nik Sultana (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 04 March 2014, 13:00-14:00

CakeML: A Verified Implementation of ML

Ramana Kumar (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 03 December 2013, 13:00-14:00

A Verified Bignum Implementation in x86-64 Machine Code

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 19 November 2013, 13:00-14:00

Mathematical practice, crowdsourcing, and social machines

Ursula Martin - Queen Mary, University of London.

Computer Laboratory, William Gates Building, Room SS03.

Monday 04 November 2013, 13:00-14:00

Some unfinished projects

Freek Wiedijk.

Computer Laboratory, William Gates Building, Room SS03.

Wednesday 14 August 2013, 13:00-14:00

Looking Back at Lyrebird

David Cock - NICTA and UNSW.

Computer Laboratory, William Gates Building, Room SS03.

Wednesday 10 July 2013, 13:00-14:00

Verified AIG Algorithms in ACL2

Jared Davis - Centaur Technologies and UT Austin.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 02 April 2013, 13:00-14:00

A Formalisation of Finite Automata in Isabelle/HOL

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 12 February 2013, 13:00-14:00

Semi-automatic Algorithm Synthesis (Case Study: Square Root)

Madalina Erascu - Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria.

Computer Laboratory, William Gates Building, Room SS03.

Thursday 21 June 2012, 13:00-14:00

Diabelli and Speedith: Heterogeneous reasoning and spider diagrams

Matej Urbas (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 19 June 2012, 13:00-14:00

Holfoot - a separation logic tool in HOL4

Thomas Tuerk - Technische Universität München.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 29 May 2012, 13:00-14:00

Diabelli: a framework for heterogeneous reasoning

Matej Urbas (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 08 May 2012, 13:00-14:00

Proof-Producing Synthesis of ML from Higher-Order Logic

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 13 March 2012, 13:00-14:00

Extending deforestation

William Sonnex (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 06 March 2012, 13:00-14:00

A Proposed Framework for Analysing Security Ceremonies

Jean Martina (Federal University of Santa Catarina / Brazil).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 28 February 2012, 13:00-14:00

Bottom-up formalization of the ARM architecture

Alastair Reid, Principal Engineer, R&D, ARM Ltd.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 21 February 2012, 13:00-14:00

Explicit vs. symbolic algorithms for solving ALFP constraints

Piotr Filipiuk - Technical University of Denmark.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 07 February 2012, 13:00-14:00

Plan B: A Buffered Memory Model for Java

David Pichardie - INRIA Rennes / Purdue University.

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 17 January 2012, 13:00-14:00

Modular verification of preemptive OS kernels

Alexey Gotsman - IMDEA Software Institute.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 08 November 2011, 13:00-14:00

On the Strength of Owicki-Gries for Resources

Alexander Malkis (IMDEA).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 01 November 2011, 13:00-14:00

Discovery of Invariants through Automated Theory Formation

Teresa Rodriguez - Heriot-Watt University.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 25 October 2011, 13:00-14:00

Zeno: An automated theorem prover for functional programs

Will Sonnex (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 11 October 2011, 13:00-14:00

Nitpicking C++ Concurrency

Jasmin Blanchette - TU München.

Computer Laboratory, William Gates Building, Room SS03.

Thursday 07 July 2011, 11:00-12:00

Work in progress: a prototype refactoring tool based on a mechanically-verified core

Nik Sultana (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 07 June 2011, 13:15-14:00

How do I know my GPU or multicore floating point computations are correct?

Miriam Leeser - Northeastern University.

Computer Laboratory, William Gates Building, Room SS03.

Wednesday 01 June 2011, 13:00-14:00

Separation Algebra

Tony Hoare - Microsoft Research.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 31 May 2011, 13:00-14:00

Title to be confirmed

Georg Struth - University of Sheffield.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 24 May 2011, 13:00-14:00

A verified runtime for a verified theorem prover

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 17 May 2011, 13:00-14:00

Using the Cambridge ARM model to verify the concrete machine code of seL4

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Thursday 28 April 2011, 13:15-14:00

Introductory meeting

William Denman (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 26 April 2011, 13:15-14:15

Validating QBF Validity in HOL4

Tjark Weber (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 15 March 2011, 13:15-14:15

Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers

Matej Urbas (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 08 March 2011, 13:15-14:15

Rough-and-ready proof reconstruction

Nik Sultana.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 01 March 2011, 13:15-14:15

The Strategy Challenge in Computer Algebra

Grant Olney Passmore (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 22 February 2011, 13:15-14:15

Formalizing Metarouting

Vilius Naudziunas.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 15 February 2011, 13:15-14:15

Quantifier Heuristics in HOL4

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 01 February 2011, 13:15-14:15

Introductory meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 18 January 2011, 13:00-14:00

Evaluating Formulas on Graphs

Anuj Dawar (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 30 November 2010, 13:00-14:00

First prototype of an Isabelle/HOL-to-LeoII interface

Nik Sultana (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 23 November 2010, 13:00-14:00

Mirage

Anil Madhavapeddy ( University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 16 November 2010, 13:00-14:00

A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions

Christian Urban (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 09 November 2010, 13:00-14:00

Formal Verification of Analog Designs using MetiTarski

William Denman (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 02 November 2010, 13:00-14:00

Bit-blasting in HOL4

Anthony Fox (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 26 October 2010, 13:00-14:00

A Simple and Efficient Memory Model for Concurrent Programming Languages

Todd Millstein (UCLA).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 19 October 2010, 13:00-14:00

Schedulability analysis of embedded real-time Java

Thomas Boegholm (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 12 October 2010, 13:00-14:00

Introductory meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 05 October 2010, 13:00-14:00

A Mechanically Verified AIG-to-BDD Conversion Algorithm

Sol Swords (University of Texas).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 06 July 2010, 13:00-14:00

General Binding in Nominal Isabelle 2

Christian Urban (TUM).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 08 June 2010, 13:00-14:00

Validating QBF Invalidity in HOL4

Tjark Weber (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 01 June 2010, 13:00-14:00

Local Reasoning about While-Loops

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 25 May 2010, 13:00-14:00

Verification of a copying garbage collector

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 18 May 2010, 13:00-14:00

Title to be confirmed

Canceled because of date clash with HCSS and workshop at MSR

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 11 May 2010, 13:00-14:00

Formal models of ARM processors in HOL

Presenters: Mike Gordon and Anthony Fox / This is a rehearsal of our HCSS talk on May 11

Mike Gordon (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 04 May 2010, 13:00-14:00

From Counter Abstraction to Thread-State Cutoffs: New Techniques for Multi-Threaded Program Verification

Thomas Wahl.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 27 April 2010, 13:00-14:00

Introductory Meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 20 April 2010, 13:00-14:00

Formal Verification of Analog and Mixed Signal Designs

Sofiene Tahar (Concordia University).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 16 March 2010, 13:00-14:00

Interfacing two similar HOLs

Nik Sultana (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 09 March 2010, 13:00-14:00

Integration of SMT Solvers with ITPs - There and Back Again

Tjark Weber (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 02 March 2010, 13:00-14:00

Verification of Multicast Protocols

Jean Martina (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 23 February 2010, 13:00-14:00

A New Version of Nominal Isabelle

Christian Urban (TUM).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 16 February 2010, 13:00-14:00

Holfoot - A separation logic tools inside HOL 4

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 26 January 2010, 13:00-14:00

Introductory meeting

Susmit Sarkar (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 19 January 2010, 13:00-14:00

Verified just-in-time compiler on x86

Notice changed date

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 15 December 2009, 13:00-14:00

jStar: Towards Practical Verification for Java

Matthew Parkinson (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 01 December 2009, 13:00-14:00

New tools in HOL 4 - Consequence Conversions, Quantifier Heuristics, Styles

Notice change of speaker

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 24 November 2009, 13:00-14:00

SMT Solvers: New Oracles for the HOL Theorem Prover

Tjark Weber (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 17 November 2009, 13:00-14:00

Abstract Threads

th orginally sheduled talk by Thomas Tuerk will probably be given next term

Alexander Malkis.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 10 November 2009, 13:00-14:00

Title to be confirmed

cancelled

Eric Koskinen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 03 November 2009, 13:00-14:00

A formal system for Euclidean diagrammatic reasoning

Jeremy Avigad (Carnegie Mellon University).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 27 October 2009, 13:00-14:00

Owicki-Gries, Thread-Modular Model-Checking, Cartesian Abstraction

Alexander Malkis.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 20 October 2009, 13:00-14:00

High-Assurance(?) High-Frequency Trading

Hasan Amjad.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 13 October 2009, 13:00-14:00

Introductory meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 06 October 2009, 13:00-14:00

Verified LISP implementations on ARM, x86 and PowerPC / A HOL Formalisation of Smallfoot

Magnus Myreen & Thomas Tuerk.

Computer Laboratory, William Gates Building, Room SS03.

Wednesday 12 August 2009, 13:00-14:00

Why you can't even trust HOL, and what to do about it

Mark Adams.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 11 August 2009, 13:00-14:00

Title to be confirmed

Canceled

Eric Koskinen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 09 June 2009, 13:00-14:00

Solving HOL problems using FOL tools

Nik Sultana (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 02 June 2009, 13:00-14:00

Verifying Flash Device Drivers

Yichi Zhang (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 26 May 2009, 13:00-14:00

Automatic Reverse Engineering for Formal Verification

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 12 May 2009, 13:00-14:00

Free to a good home: an advertisement for the "new" HOL4 theories of probability, integration, and information. / A Heap of Problems

Aaron R. Coble / Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 05 May 2009, 13:00-14:00

Mechanically Proving Hoare Formulae

Mike Gordon (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 28 April 2009, 13:00-14:00

Introductory Meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 21 April 2009, 13:00-14:00

Formal Verification of Centaur Technology's X86-Compatible Media Unit

Warren A. Hunt (University of Texas).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 31 March 2009, 13:00-14:00

A Verifiable, Executable SLR Parser

Aditi Barthwal (The Australian National University).

Computer Laboratory, William Gates Building, Room SS03.

Thursday 19 March 2009, 12:30-13:30

A Theory of Type-directed Coercion Insertion

Note change of date

Mike Hicks (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 17 March 2009, 13:00-14:00

Semantics Lunch

Canceled, semantics lunch instead

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 10 March 2009, 13:00-14:00

Modular verification of concurrent programs with heap

Mike Hick's talk moved to the 17th of March

Alexey Gotsman (ARG).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 03 March 2009, 13:00-14:00

Formal power series in Isabelle/HOL

Amine Chaieb (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 24 February 2009, 13:00-14:00

RGSep action inference

Viktor Vafeiadis (Microsoft Research Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 17 February 2009, 13:00-14:00

Verifying Distributed Systems: the Operational Approach

Tom Ridge (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 10 February 2009, 13:00-14:00

Finite Model Generation, Proof-Producing SAT Solvers, and SMT

Tjark Weber (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 03 February 2009, 13:00-14:00

A HOL Formalisation of Smallfoot

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 27 January 2009, 13:00-14:00

Title to be confirmed

Canceled because of POPL

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 20 January 2009, 13:00-14:00

Introductory Meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 13 January 2009, 13:00-14:00

An ACL2 Tutorial

Matt Kaufmann (University of Texas at Austin).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 02 December 2008, 13:00-14:00

The Semantics of x86-CC Multiprocessor Machine Code

Susmit Sarkar (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 25 November 2008, 13:00-14:00

Techniques for Symbolic Complexity Bounds

Eric Koskinen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 18 November 2008, 13:00-14:00

Mechanically verified LISP interpreters

Note unusual time

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 11 November 2008, 12:00-13:00

Proving recursive programs terminating

Dr Byron Cook (Microsoft Research).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 04 November 2008, 13:00-14:00

Towards Automatic Stability Analysis for Rely-Guarantee Proofs

Hasan Amjad (Middlesex University).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 28 October 2008, 13:00-14:00

The Mechanical Formalization of Measure, Integration and Probability

David Lester (University of Manchester).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 21 October 2008, 13:00-14:00

Applications of MetiTarski in the Verification of Control and Hybrid Systems

Behzad Akbarpour (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 14 October 2008, 13:00-14:00

Introductory Meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 07 October 2008, 13:00-14:00

Formal Methods for Critical Systems

Steve Miller (Rockwell Collins).

Computer Laboratory, William Gates Building, Room SS03.

Thursday 18 September 2008, 14:00-15:00

Diagrammatic Reasoning in Separation Logic

Matt Ridsdale (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Wednesday 17 September 2008, 13:00-14:00

ACL2-Based Verification of NoC Communication Infrastructures

Laurence Pierre (TIMA).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 17 June 2008, 13:00-14:00

The Relative Consistency of the Axiom of Choice, Mechanized Using Isabelle/ZF

Lawrence Paulson (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 10 June 2008, 13:00-14:00

Proving Liveness Properties of Non-blocking Data Structures

Alexey Gotsman (ARG).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 03 June 2008, 13:00-14:00

Proof-producing decompilation and compilation

Room changed

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 27 May 2008, 13:00-14:00

Proving conditional termination

Dr Byron Cook (Microsoft Research).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 20 May 2008, 13:00-14:00

Applying Machine Learning to Heuristic Selection in an Automated Theorem Prover

James Bridge (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 13 May 2008, 13:00-14:00

Information, Anonymity, and Proof

Aaron Coble (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 06 May 2008, 13:00-14:00

LCF-style Propositional Simplification With BDDs and SAT Solvers

Hasan Amjad (Middlesex University).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 29 April 2008, 13:00-14:00

Introductory Meeting

-.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 22 April 2008, 13:00-14:00

A Constraint-Programming Framework For Bounded Program Verification

Helene Collavizza (Ecole Polytechnique Universitaire de Nice Sophia Antipolis).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 11 March 2008, 13:00-14:00

Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II

Christoph Benzmueller ().

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 04 March 2008, 13:00-14:00

Some "Real World" Problems in the Analog and Mixed Signal Domains

Kevin Jones (Rambus).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 26 February 2008, 13:00-14:00

An Embedding of Abstract Separation Logic in HOL

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 19 February 2008, 13:00-14:00

A rigorous approach to networking: TCP, from implementation to protocol to service

Tom Ridge (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 12 February 2008, 13:00-14:00

Automatic Proof for Theorems On Transcendental Functions

Lawrence Paulson (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 05 February 2008, 13:00-14:00

Title to be confirmed

Canceled

Samin Ishtiaq (Currently: ARM).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 29 January 2008, 13:00-14:00

MaLARea: a Metasystem for Automated Reasoning in Large Theories

Josef Urban (Charles University).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 22 January 2008, 13:00-14:00

Introductory Meeting

Speaker to be confirmed.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 15 January 2008, 13:00-14:00

CANCELED !!!

Canceled

Christoph Benzmueller ().

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 11 December 2007, 13:00-14:00

Automatic proof of SPARK verification conditions

Paul Jackson (School of Informatics, University of Edinburgh).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 11 December 2007, 13:00-14:00

n-bit words in HOL

Anthony Fox (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 04 December 2007, 13:00-14:00

Proving Correctness of Secret Sharing Protocols using the Inductive Method

Jean Martina (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 27 November 2007, 13:00-14:00

From Program Logics to Program Analyses And Back

Alexey Gotsman (ARG).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 20 November 2007, 13:00-14:00

Reasoning about Linear Systems

Rob Arthan (Lemma 1).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 13 November 2007, 13:00-14:00

Synthesis from Temporal Specifications

Nir Piterman (Imperial College London).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 06 November 2007, 13:00-14:00

A tool for verification: A decompiler from ARM to HOL

Magnus Myreen (University of Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 30 October 2007, 13:00-14:00

A modular formalisation of finite group theory

Georges Gonthier (Microsoft Research).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 23 October 2007, 13:00-14:00

Executable Biology: Towards Computer Programs that Mimic Life

Jasmin Fisher (MSR Cambridge).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 16 October 2007, 13:00-14:00

Introductiory Meeting

.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 09 October 2007, 11:00-12:00

Verifying an Operating System Kernel

Room changed

Michael Norrish (Nicta).

Lecture Theatre 1, Computer Laboratory, William Gates Building.

Thursday 27 September 2007, 14:00-15:00

Boosting Verification by Automatic Tuning of Decision Procedures

Domagoj Babic (University of British Columbia).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 18 September 2007, 13:00-14:00

Cryptanalysis with SAT - a propositional programming environment

Room changed

Mateusz Srebrny.

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 14 August 2007, 13:00-14:00

One-pass Tableaux for Computation Tree Logic

Room changed

Rajeev Goré (Australian National University).

Computer Laboratory, William Gates Building, Room SS03.

Tuesday 07 August 2007, 13:00-14:00

Progress Report on Leo-II, an Automatic Theorem Prover for Higher-Order Logic

Christoph Benzmueller.

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 03 July 2007, 13:00-14:00

A Deep Embedding of a Decidable Fragment of Separation Logic in HOL

Thomas Tuerk (University of Cambridge).

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 26 June 2007, 13:00-14:00

The ARM Cortex-M1 Architecture in Coq

Samin Ishtiaq (Currently: ARM).

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 19 June 2007, 13:00-14:00

From QED to X-Logic, following the lead of Leibniz

Roger Bishop Jones (None).

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 12 June 2007, 13:00-14:00

Connecting Partial and Total Correctness for Probabilistic Programs in HOL4

Aaron Coble (University of Cambridge).

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 05 June 2007, 13:00-14:00

A Compressing Translation from Propositional Resolution to Natural Deduction

Hasan Amjad (University of Cambridge).

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 29 May 2007, 13:00-14:00

Local Reasoning for Storable Locks and Threads

Alexey Gotsman (University of Cambridge).

Computer Laboratory, William Gates Building, Room GS15.

Tuesday 15 May 2007, 13:00-14:00