University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Computer Laboratory Automated Reasoning Group Lunches

Further detail
Subscribe using ical/vcal (Help)

Tuesdays at 1:00 pm in William Gates Building, Room SS03 , the Automated Reasoning Group holds an informal group meeting over lunch. For details please have a look at http://www.cl.cam.ac.uk/research/hvg/ARG_Lunches/.

If you have a question about this list, please contact: William Denman. If you have a question about a specific talk, click on that talk to find its organiser.

0 upcoming talks and 145 talks in the archive.

Logic programming beyond Prolog

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

UserMaarten van Emden ( University of Victoria, Canada).

HouseSeminar Room, Microsoft Research, Station Road, Cambridge.

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

Interfacing and improving proof tools

UserNik Sultana (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

CakeML: A Verified Implementation of ML

UserRamana Kumar (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Verified Bignum Implementation in x86-64 Machine Code

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Mathematical practice, crowdsourcing, and social machines

UserUrsula Martin - Queen Mary, University of London.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Some unfinished projects

UserFreek Wiedijk.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Looking Back at Lyrebird

UserDavid Cock - NICTA and UNSW.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Verified AIG Algorithms in ACL2

UserJared Davis - Centaur Technologies and UT Austin.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Formalisation of Finite Automata in Isabelle/HOL

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

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

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Diabelli and Speedith: Heterogeneous reasoning and spider diagrams

UserMatej Urbas (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Holfoot - a separation logic tool in HOL4

UserThomas Tuerk - Technische Universität München.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Diabelli: a framework for heterogeneous reasoning

UserMatej Urbas (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Proof-Producing Synthesis of ML from Higher-Order Logic

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Extending deforestation

UserWilliam Sonnex (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Proposed Framework for Analysing Security Ceremonies

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

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Bottom-up formalization of the ARM architecture

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

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Explicit vs. symbolic algorithms for solving ALFP constraints

UserPiotr Filipiuk - Technical University of Denmark.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Plan B: A Buffered Memory Model for Java

UserDavid Pichardie - INRIA Rennes / Purdue University.

HouseComputer Laboratory, William Gates Building, Room GS15.

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

Modular verification of preemptive OS kernels

UserAlexey Gotsman - IMDEA Software Institute.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

On the Strength of Owicki-Gries for Resources

UserAlexander Malkis (IMDEA).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Discovery of Invariants through Automated Theory Formation

UserTeresa Rodriguez - Heriot-Watt University.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Zeno: An automated theorem prover for functional programs

UserWill Sonnex (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Nitpicking C++ Concurrency

UserJasmin Blanchette - TU München.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserNik Sultana (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserMiriam Leeser - Northeastern University.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Separation Algebra

UserTony Hoare - Microsoft Research.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Title to be confirmed

UserGeorg Struth - University of Sheffield.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A verified runtime for a verified theorem prover

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory meeting

UserWilliam Denman (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Validating QBF Validity in HOL4

UserTjark Weber (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers

UserMatej Urbas (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Rough-and-ready proof reconstruction

UserNik Sultana.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

The Strategy Challenge in Computer Algebra

UserGrant Olney Passmore (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Formalizing Metarouting

UserVilius Naudziunas.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Quantifier Heuristics in HOL4

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Evaluating Formulas on Graphs

UserAnuj Dawar (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserNik Sultana (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Mirage

UserAnil Madhavapeddy ( University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserChristian Urban (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Formal Verification of Analog Designs using MetiTarski

UserWilliam Denman (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Bit-blasting in HOL4

UserAnthony Fox (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Simple and Efficient Memory Model for Concurrent Programming Languages

UserTodd Millstein (UCLA).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Schedulability analysis of embedded real-time Java

UserThomas Boegholm (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Mechanically Verified AIG-to-BDD Conversion Algorithm

UserSol Swords (University of Texas).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

General Binding in Nominal Isabelle 2

UserChristian Urban (TUM).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Validating QBF Invalidity in HOL4

UserTjark Weber (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Local Reasoning about While-Loops

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Verification of a copying garbage collector

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Title to be confirmed

Canceled because of date clash with HCSS and workshop at MSR

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 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

UserMike Gordon (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserThomas Wahl.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory Meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Formal Verification of Analog and Mixed Signal Designs

UserSofiene Tahar (Concordia University).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Interfacing two similar HOLs

UserNik Sultana (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Integration of SMT Solvers with ITPs - There and Back Again

UserTjark Weber (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Verification of Multicast Protocols

UserJean Martina (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A New Version of Nominal Isabelle

UserChristian Urban (TUM).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Holfoot - A separation logic tools inside HOL 4

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory meeting

UserSusmit Sarkar (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Verified just-in-time compiler on x86

Notice changed date

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

jStar: Towards Practical Verification for Java

UserMatthew Parkinson (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

Notice change of speaker

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

SMT Solvers: New Oracles for the HOL Theorem Prover

UserTjark Weber (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Abstract Threads

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

UserAlexander Malkis.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Title to be confirmed

cancelled

UserEric Koskinen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A formal system for Euclidean diagrammatic reasoning

UserJeremy Avigad (Carnegie Mellon University).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserAlexander Malkis.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

High-Assurance(?) High-Frequency Trading

UserHasan Amjad.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserMagnus Myreen & Thomas Tuerk.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserMark Adams.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Title to be confirmed

Canceled

UserEric Koskinen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Solving HOL problems using FOL tools

UserNik Sultana (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Verifying Flash Device Drivers

UserYichi Zhang (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Automatic Reverse Engineering for Formal Verification

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 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

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

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Mechanically Proving Hoare Formulae

UserMike Gordon (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory Meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserWarren A. Hunt (University of Texas).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Verifiable, Executable SLR Parser

UserAditi Barthwal (The Australian National University).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Theory of Type-directed Coercion Insertion

Note change of date

UserMike Hicks (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Semantics Lunch

Canceled, semantics lunch instead

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Modular verification of concurrent programs with heap

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

UserAlexey Gotsman (ARG).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Formal power series in Isabelle/HOL

UserAmine Chaieb (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

RGSep action inference

UserViktor Vafeiadis (Microsoft Research Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Verifying Distributed Systems: the Operational Approach

UserTom Ridge (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserTjark Weber (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A HOL Formalisation of Smallfoot

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Title to be confirmed

Canceled because of POPL

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory Meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

An ACL2 Tutorial

UserMatt Kaufmann (University of Texas at Austin).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

The Semantics of x86-CC Multiprocessor Machine Code

UserSusmit Sarkar (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Techniques for Symbolic Complexity Bounds

UserEric Koskinen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Mechanically verified LISP interpreters

Note unusual time

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Proving recursive programs terminating

UserDr Byron Cook (Microsoft Research).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Towards Automatic Stability Analysis for Rely-Guarantee Proofs

UserHasan Amjad (Middlesex University).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

The Mechanical Formalization of Measure, Integration and Probability

UserDavid Lester (University of Manchester).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Applications of MetiTarski in the Verification of Control and Hybrid Systems

UserBehzad Akbarpour (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory Meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Formal Methods for Critical Systems

UserSteve Miller (Rockwell Collins).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Diagrammatic Reasoning in Separation Logic

UserMatt Ridsdale (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

ACL2-Based Verification of NoC Communication Infrastructures

UserLaurence Pierre (TIMA).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserLawrence Paulson (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Proving Liveness Properties of Non-blocking Data Structures

UserAlexey Gotsman (ARG).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Proof-producing decompilation and compilation

Room changed

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room GS15.

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

Proving conditional termination

UserDr Byron Cook (Microsoft Research).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Applying Machine Learning to Heuristic Selection in an Automated Theorem Prover

UserJames Bridge (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Information, Anonymity, and Proof

UserAaron Coble (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

LCF-style Propositional Simplification With BDDs and SAT Solvers

UserHasan Amjad (Middlesex University).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory Meeting

User-.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A Constraint-Programming Framework For Bounded Program Verification

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

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserChristoph Benzmueller ().

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserKevin Jones (Rambus).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

An Embedding of Abstract Separation Logic in HOL

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserTom Ridge (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Automatic Proof for Theorems On Transcendental Functions

UserLawrence Paulson (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Title to be confirmed

Canceled

UserSamin Ishtiaq (Currently: ARM).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

MaLARea: a Metasystem for Automated Reasoning in Large Theories

UserJosef Urban (Charles University).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductory Meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

CANCELED !!!

Canceled

UserChristoph Benzmueller ().

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Automatic proof of SPARK verification conditions

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

HouseComputer Laboratory, William Gates Building, Room SS03.

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

n-bit words in HOL

UserAnthony Fox (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Proving Correctness of Secret Sharing Protocols using the Inductive Method

UserJean Martina (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

From Program Logics to Program Analyses And Back

UserAlexey Gotsman (ARG).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Reasoning about Linear Systems

UserRob Arthan (Lemma 1).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Synthesis from Temporal Specifications

UserNir Piterman (Imperial College London).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A tool for verification: A decompiler from ARM to HOL

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

A modular formalisation of finite group theory

UserGeorges Gonthier (Microsoft Research).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Executable Biology: Towards Computer Programs that Mimic Life

UserJasmin Fisher (MSR Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Introductiory Meeting

User.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Verifying an Operating System Kernel

Room changed

UserMichael Norrish (Nicta).

HouseLecture Theatre 1, Computer Laboratory, William Gates Building.

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

Boosting Verification by Automatic Tuning of Decision Procedures

UserDomagoj Babic (University of British Columbia).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

Cryptanalysis with SAT - a propositional programming environment

Room changed

UserMateusz Srebrny.

HouseComputer Laboratory, William Gates Building, Room SS03.

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

One-pass Tableaux for Computation Tree Logic

Room changed

UserRajeev Goré (Australian National University).

HouseComputer Laboratory, William Gates Building, Room SS03.

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

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

UserChristoph Benzmueller.

HouseComputer Laboratory, William Gates Building, Room GS15.

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

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

UserThomas Tuerk (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room GS15.

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

The ARM Cortex-M1 Architecture in Coq

UserSamin Ishtiaq (Currently: ARM).

HouseComputer Laboratory, William Gates Building, Room GS15.

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

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

UserRoger Bishop Jones (None).

HouseComputer Laboratory, William Gates Building, Room GS15.

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

Connecting Partial and Total Correctness for Probabilistic Programs in HOL4

UserAaron Coble (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room GS15.

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

A Compressing Translation from Propositional Resolution to Natural Deduction

UserHasan Amjad (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room GS15.

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

Local Reasoning for Storable Locks and Threads

UserAlexey Gotsman (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room GS15.

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

Please see above for contact details for this list.

Other lists

Type the title of a new list here Cambridge University Astronomical Society (CUAS) GS5, Donald McIntyre Building, Faculty of Education, 184 Hills Road, Cambridge

Other talks

Title to be confirmed Group Work title abstract tba Security Cooperation within Government and between Governments Title abstract tbc Science & the Public in Action: Can and should climate scientists be activists?
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity