Publications

2016

https://privat.thomas-tuerk.de/assets/publications/FM2016.bib https://privat.thomas-tuerk.de/assets/publications/FM2016.pdf Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, Cesar Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk
Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor
FM 2016

2015

https://privat.thomas-tuerk.de/assets/publications/TuMyKu15.bib https://privat.thomas-tuerk.de/assets/publications/TuMyKu15.pdf T. Tuerk and M. Myreen and R. Kumar
Pattern Matches in HOL: A New Representation and Improved Code Generation
ITP 2015
https://privat.thomas-tuerk.de/assets/publications/RidgeSTGMS15.bib http://sigops.org/sosp/sosp15/current/2015-Monterey/printable/102-ridge.pdf Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, Peter Sewell
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems
SOSP 2015

2012

https://privat.thomas-tuerk.de/assets/publications/LamTue12.bib https://privat.thomas-tuerk.de/assets/publications/LamTue12.pdf P. Lammich and T. Tuerk
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm
ITP 2012

2011

https://privat.thomas-tuerk.de/assets/publications/Tuer10PhD.bib http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-799.pdf T. Tuerk
A Separation Logic Framework for HOL
PhD thesis, Technical Report

2010

https://privat.thomas-tuerk.de/assets/publications/Tuer10.bib https://privat.thomas-tuerk.de/assets/talks/vstte10.pdf T. Tuerk
Local Reasoning about While-Loops
Verified Software: Theories, Tools and Experiments 2010 - Theory Workshop

2009

https://privat.thomas-tuerk.de/assets/publications/Tuer09.bib https://privat.thomas-tuerk.de/assets/publications/Tuer09.pdf T. Tuerk
A formalisation of Smallfoot in HOL
Theorem Proving in Higher Order Logics (TPHOLs)

2008

https://privat.thomas-tuerk.de/assets/publications/Tuer08.bib https://privat.thomas-tuerk.de/assets/publications/Tuer08.pdf T. Tuerk
A Separation Logic Framework in HOL
Theorem Proving in Higher Order Logics (TPHOLs) : Emerging Trends

2007

https://privat.thomas-tuerk.de/assets/publications/TuSG07.bib https://privat.thomas-tuerk.de/assets/publications/TuSG07.pdf T. Tuerk and K. Schneider and M. Gordon
Model Checking PSL Using HOL and SMV
Haifa Verification Conference (HVC)

2005

https://privat.thomas-tuerk.de/assets/publications/SBST05a.bib https://privat.thomas-tuerk.de/assets/publications/SBST05a.pdf K. Schneider and J. Brandt and T. Schuele and T. Tuerk
Improving Constructiveness in Code Generators
Synchronous Languages, Applications, and Programming (SLAP)
https://privat.thomas-tuerk.de/assets/publications/SBST05b.bib https://privat.thomas-tuerk.de/assets/publications/SBST05b.pdf K. Schneider and J. Brandt and T. Schuele and T. Tuerk
Maximal Causality Analysis
Application of Concurrency to System Design (ACSD)
https://privat.thomas-tuerk.de/assets/publications/TuSc05.bib https://privat.thomas-tuerk.de/assets/publications/TuSc05.pdf T. Tuerk and K. Schneider
From PSL to LTL: A Formal Validation in HOL
Theorem Proving in Higher Order Logic (TPHOL)
https://privat.thomas-tuerk.de/assets/publications/TuSc05a.bib https://privat.thomas-tuerk.de/assets/publications/TuSc05a.pdf T. Tuerk and K. Schneider
Relationship between Alternating omega-Automata and Symbolically Represented Nondeterministic omega-Automata
Technical Report
https://privat.thomas-tuerk.de/assets/publications/Tuer05.bib https://privat.thomas-tuerk.de/assets/publications/Tuer05.pdf T. Tuerk
A Hierarchy for Accellera's Property Specification Language
Master Thesis