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 |