Thomas Tuerk

Name:	Thomas Tuerk
Affiliation:	University of Cambridge
E-mail:	(only provided to users who are logged into talks.cam)
Last login:	28 Jan 2013, 11:09 a.m.

Public lists managed by Thomas Tuerk

Talks given by Thomas Tuerk

Obviously this only lists talks that are listed through talks.cam. Furthermore, this facility only works if the speaker's e-mail was specified in a talk. Most talks have not done this.

• An Embedding of Abstract Separation Logic in HOL
• A Deep Embedding of a Decidable Fragment of Separation Logic in HOL

Talks organised by Thomas Tuerk

This list is based on what was entered into the 'organiser' field in a talk. It may not mean that Thomas Tuerk actually organised the talk, they may have been responsible only for entering the talk into the talks.cam system.

• A Verifiable, Executable SLR Parser
• An ACL2 Tutorial
• The Semantics of x86-CC Multiprocessor Machine Code
• Techniques for Symbolic Complexity Bounds
• Mechanically verified LISP interpreters
• Proving recursive programs terminating
• Towards Automatic Stability Analysis for Rely-Guarantee Proofs
• The Mechanical Formalization of Measure, Integration and Probability
• Applications of MetiTarski in the Verification of Control and Hybrid Systems
• Introductory Meeting
• Formal Methods for Critical Systems
• Diagrammatic Reasoning in Separation Logic
• ACL2-Based Verification of NoC Communication Infrastructures
• The Relative Consistency of the Axiom of Choice, Mechanized Using Isabelle/ZF
• Proving Liveness Properties of Non-blocking Data Structures
• Proof-producing decompilation and compilation
• Proving conditional termination
• Applying Machine Learning to Heuristic Selection in an Automated Theorem Prover
• Information, Anonymity, and Proof
• LCF-style Propositional Simplification With BDDs and SAT Solvers
• Introductory Meeting
• A Constraint-Programming Framework For Bounded Program Verification
• Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II
• Some "Real World" Problems in the Analog and Mixed Signal Domains
• An Embedding of Abstract Separation Logic in HOL
• A rigorous approach to networking: TCP, from implementation to protocol to service
• Automatic Proof for Theorems On Transcendental Functions
• Title to be confirmed
• MaLARea: a Metasystem for Automated Reasoning in Large Theories
• Introductory Meeting
• Automatic proof of SPARK verification conditions
• Automatic proof of SPARK verification conditions
• CANCELED !!!
• n-bit words in HOL
• Proving Correctness of Secret Sharing Protocols using the Inductive Method
• From Program Logics to Program Analyses And Back
• Reasoning about Linear Systems
• Synthesis from Temporal Specifications
• A tool for verification: A decompiler from ARM to HOL
• A modular formalisation of finite group theory
• Executable Biology: Towards Computer Programs that Mimic Life
• Introductiory Meeting
• Verifying an Operating System Kernel
• Boosting Verification by Automatic Tuning of Decision Procedures
• Cryptanalysis with SAT - a propositional programming environment
• One-pass Tableaux for Computation Tree Logic
• Progress Report on Leo-II, an Automatic Theorem Prover for Higher-Order Logic
• A Deep Embedding of a Decidable Fragment of Separation Logic in HOL
• The ARM Cortex-M1 Architecture in Coq
• From QED to X-Logic, following the lead of Leibniz
• Connecting Partial and Total Correctness for Probabilistic Programs in HOL4
• A Compressing Translation from Propositional Resolution to Natural Deduction
• Local Reasoning for Storable Locks and Threads
• Local Reasoning for Storable Locks and Threads