| Address [vCard]: |
Technische Universität München Institut für Informatik Boltzmannstr. 3 85748 Garching Deutschland |
|---|---|
| Telephone: | +49 (89) 289-17330 |
| Telefax: | +49 (89) 289-17307 |
| Office: | MI 01.11.057 |
Publications
2011
|
|
|
T. Tuerk A Separation Logic Framework for HOL PhD thesis, Technical Report |
2010
|
|
|
T. Tuerk Local Reasoning about While-Loops Verified Software: Theories, Tools and Experiments 2010 - Theory Workshop |
2009
|
|
|
T. Tuerk A formalisation of Smallfoot in HOL Theorem Proving in Higher Order Logics (TPHOLs) |
2008
|
|
|
T. Tuerk A Separation Logic Framework in HOL Theorem Proving in Higher Order Logics (TPHOLs) : Emerging Trends |
2007
|
|
|
T. Tuerk and K. Schneider and M. Gordon Model Checking PSL Using HOL and SMV Haifa Verification Conference (HVC) |
2005
|
|
|
K. Schneider and J. Brandt and T. Schuele and T. Tuerk Improving Constructiveness in Code Generators Synchronous Languages, Applications, and Programming (SLAP) |
|
|
|
|
K. Schneider and J. Brandt and T. Schuele and T. Tuerk Maximal Causality Analysis Application of Concurrency to System Design (ACSD) |
|
|
|
|
T. Tuerk and K. Schneider From PSL to LTL: A Formal Validation in HOL Theorem Proving in Higher Order Logic (TPHOL) |
|
|
|
|
T. Tuerk and K. Schneider Relationship between Alternating omega-Automata and Symbolically Represented Nondeterministic omega-Automata Technical Report |
|
|
|
|
T. Tuerk A Hierarchy for Accellera's Property Specification Language Master Thesis |
2003
|
|
|
T. Tuerk Constraintbasierte Vervollständigungstechniken: Gleichheitsconstraints Project Thesis |
Talks
| 29 Feb. 2012 | Club2 | |
|
A Formalisation of Finite Automata in Isabelle/HOL (slides, printer version) |
||
| 1 Feb. 2011 | ARG Lunch | |
|
Quantifier Heurististics in HOL4 (slides, printer version) |
||
| 18 Aug. 2010 | VSTTE'10 - Theory Workshop | |
|
Local Reasoning about While-Loops (slides, paper) |
||
| 26 Jan. 2010 | ARG Lunch | |
|
A demo of Holfoot (slides, printer version) |
||
| 24 Nov. 2009 | ARG Lunch | |
|
A presentation of some tools used for Holfoot (slides, printer version) |
||
| 19 Aug. 2009 | TPHOLs | |
|
A formalisation of Smallfoot in HOL (slides, printer version) |
||
| 5 May 2009 | ARG Lunch | |
|
A Heap of Problems (slides, printer version) |
||
| 27 Jan. 2009 | ARG Lunch | |
|
A HOL implementation of Smallfoot (slides, printer version) |
||
| 2 Sep. 2008 | Research & review meeting | |
|
A fully-expansive HOL implementation of Smallfoot (slides, printer version) |
||
| 19 Feb. 2008 | ARG Lunch | |
|
An Embedding of Abstract Separation Logic in HOL (slides, printer version) |
||
| 26 Jun. 2007 | ARG Lunch | |
|
A Deep Embedding of a Decidable Fragment of Separation Logic in HOL (slides, detailed documentation) |
||
| 7 Nov. 2006 | ARG Lunch | |
|
A verifying ARM compiler (slides, printer version) |
||
| 23 Oct. 2006 | Haifa Verification Conference | |
|
Model Checking PSL using HOL and SMV (slides, printer version) |
||
| 21 Jun. 2006 | ARG Lunch | |
|
Deep Embeddings of Temporal Logics in HOL (slides, printer version) |
||
| 1 Feb. 2006 | ARG Lunch | |
|
PSL in HolCheck (slides, printer version) |
||
| 23 Aug. 2005 | TPHOLs | |
| From PSL to LTL: A Formal Validation in HOL (slides, printer version) | ||
Posters
- A Heap of Problems
- Holfoot (previous versions 1, 2)
- PSL
Projects
I'm a member of the CAVA project. In the past, I developed Holfoot, a formalisation of the separation logic tool Smallfoot in HOL4. Moreover I'm the admin of A Heap of Problems, a wiki that collects benchmark problems for separation logic tools.
Links
- CAVA
- Holfoot
- Heap of Problems Wiki
- Personal Webpage
- Computer Lab of the University of Cambridge
- Embedded Systems Group of TU Kaiserslautern
- My Page at the Computer Lab
- My Page at the Embedded Systems Group