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
![[Talks.cam]](/static/images/talkslogosmall.gif)
