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

Computer Laboratory Automated Reasoning Group Lunches

Add to your list(s) Send you e-mail reminders 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/.

Tell a friend about this list:

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 144 talks in the archive.

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

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

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

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

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

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

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

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

Introductory meeting

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 06 October 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

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

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

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

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

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

Information, Anonymity, and Proof

UserAaron Coble (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 06 May 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

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

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

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

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

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

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

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

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.

 

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