Publications

2016

BibTeX 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

BibTeX PDF     T. Tuerk and M. Myreen and R. Kumar
Pattern Matches in HOL: A New Representation and Improved Code Generation
ITP 2015
BibTeX 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

BibTeX PDF     P. Lammich and T. Tuerk
Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm
ITP 2012

2011

BibTeX PDF     T. Tuerk
A Separation Logic Framework for HOL
PhD thesis, Technical Report

2010

BibTeX PDF     T. Tuerk
Local Reasoning about While-Loops
Verified Software: Theories, Tools and Experiments 2010 - Theory Workshop

2009

BibTeX PDF   T. Tuerk
A formalisation of Smallfoot in HOL
Theorem Proving in Higher Order Logics (TPHOLs)

2008

BibTeX PDF   T. Tuerk
A Separation Logic Framework in HOL
Theorem Proving in Higher Order Logics (TPHOLs) : Emerging Trends

2007

BibTeX PDF   T. Tuerk and K. Schneider and M. Gordon
Model Checking PSL Using HOL and SMV
Haifa Verification Conference (HVC)

2005

BibTeX PDF   K. Schneider and J. Brandt and T. Schuele and T. Tuerk
Improving Constructiveness in Code Generators
Synchronous Languages, Applications, and Programming (SLAP)
BibTeX PDF   K. Schneider and J. Brandt and T. Schuele and T. Tuerk
Maximal Causality Analysis
Application of Concurrency to System Design (ACSD)
BibTeX PDF   T. Tuerk and K. Schneider
From PSL to LTL: A Formal Validation in HOL
Theorem Proving in Higher Order Logic (TPHOL)
BibTeX PDF   T. Tuerk and K. Schneider
Relationship between Alternating omega-Automata and Symbolically Represented Nondeterministic omega-Automata
Technical Report
BibTeX PDF   T. Tuerk
A Hierarchy for Accellera's Property Specification Language
Master Thesis

2003

BibTeX PDF   T. Tuerk
Constraintbasierte Vervollständigungstechniken: Gleichheitsconstraints
Project Thesis