Thomas Tuerk

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

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.

• A Formalisation of Finite Automata in Isabelle/HOL
• A Formalisation of Finite Automata in Isabelle/HOL
• Quantifier Heuristics in HOL4
• Local Reasoning about While-Loops
• Holfoot - A separation logic tools inside HOL 4
• New tools in HOL 4 - Consequence Conversions, Quantifier Heuristics, Styles
• Abstract Threads
• A HOL Formalisation of Smallfoot
• 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
• CANCELED !!!
• Automatic proof of SPARK verification conditions
• Automatic proof of SPARK verification conditions
• 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