German (native speaker), English (full professional proficiency)
databases (esp. MySQL and MS SQL Server), Git, XML, HTML, CSS, JSON, Docker, ...
expert for HOL 4 theorem prover, experienced user of Isabelle/HOL and Coq
experience with model-based-testing, one of the developers of Lem; developer of Adatt; I helped with specifying POSIX filesystems (http://www.tom-ridge.com/filesystems.html)
experience with verification of low level code, e.g. hardering a microhypervisor using Coq or building a transpiler for maschine code; experience with temporal logics and model checking
I helped develop a program refinement framework in Isabelle/HOL; design of a simple program refinement framework in Coq that was used to harden a micro-hypervisor (https://privat.thomas-tuerk.de/assets/publications/FM2016.pdf);
teaching a master course about interactive theorem proving at KTH in Stockholm (slides)
Freelancer, IT Dienstleistungen Dr. Thomas Türk, Brechen, Germany.
Developer, F+S Fleckner und Simon Informationstechnik GmbH, Limburg, Germany.
software developer, et-systems GmbH, Limburg, Germany.
working part time (20 h / week) on customising the ERP System APplus, this involved coding some web-frontend (Javacript, CSS, HTML) in ASP.NET (mainly C#) as well as backend work with an Java application server and a Microsoft SQL server
Independent Scholar, Brechen, Germany.
developemnt of ADATT, a tool to help domain-experts write formal specifications
Postdoktor, KTH, Stockholm, Sweden.
working for Prof. Dam, giving a course on HOL 4, implementing a transpiler from assembler code to a binary intermediate language in HOL 4
Formal Methods Staff Engineer, FireEye, Dresden, Germany.
working on verifying a micro-hypervisor, using program refinement, a formal Coq model and Coq proofs as well as conformance testing
Computer Science Engineer, University of Leicester, Leicester, UK.
working with Dr. Tom Ridge on project The future filesystems project; using Lem, I helped to formalise POSIX filesystems and test this formalisation
Research Associate, University of Cambridge, Cambridge, UK.
working with Prof. Peter Sewell on project Rigorous Engineering for Mainstream Systems, in particular on tool Lem
Wissenschaftlicher Mitarbeiter, TU München, Munich, Germany.
working with Prof. Tobias Nipkow on the CAVA project
Research Assistant, University of Cambridge, Cambridge, UK.
working part-time for Matthew Parkinson on separation logic tool JStar while finishing my Ph.D. thesis
Ph.D., University of Cambridge, Cambridge, UK.
supervised by Prof. Mike Gordon, thesis title A Separation Logic Framework for HOL; started in parallel with diploma studies in Kaiserslautern under supervision of Prof. Schneider, moved to Cambridge in Jan. 2007
Diplom, University of Kaiserslautern, Kaiserslautern, Germany.
supervisor Prof. K. Schneider, thesis title A Hierarchy for Accellera's Property Specification Language betreut von Prof. K. Schneider
Abitur (German university entrance qualification), Tilemannschule Limburg, Limburg, Germany.
||Dr. Thomas Tuerk|
|phone||+49 6483 803150|
I believe that an informal email or a phone call are best suited to get in contact. After initial contact, we can a use other communication channels (like common video conferencing platforms) or meet in person. For existing customers, my Helpdesk might also be useful.
If you are looking for information that is not or only indirectly related to my work as a freelancer, you should have a look at my personal webpage (https://privat.thomas-tuerk.de/en). You can find personal contact details or a list of my publications there.
Here you can find some selected projects of mine:
Prüfungsplaner is a desktop application used for scheduling oral exams at German high schools, which I have been developing in 2022. Given a list of exams together with information about resources that can be used (rooms, teachers, timeslots, ...) as well as preferences, Prüfungsplaner produces schedules for these exams. A schedule consists of an assignment of a room, a timeslot and teachers to an exam. Using genetic algorithms, Prüfungsplaner attempts to find good schedules quickly. Thereby it is highly non-trivial to define precisely what constitutes a good schedule. Prüfungsplaner is available with and without graphical user-interface for MS Windows and Linux. More details as well as download links of a demo version are available on a separate page. Since Prüfungsplaner is specifically tailored to the needs of German high schools, this separate page as well as Prüfungsplaner itself are only available in German.
I'm interested in simplifying communication between domain experts and formal-methods experts. In order to use interactive theorem proving (ITP) on real world problems, correct and detailled models of real world artifacts like processors or programming languages are needed. Creating such models is a lot of work and the needed details are only known to experts of these real-world systems. Such domain-experts are usually not experts for formal methods or ITP and therefore. Such ITP expertise is however needed to create good formal models. I'm interested in how domain and formal method experts can cooperate to create such formal models.
I got interested in this topic while working for Prof. Peter Sewell on Lem. Lem is a tool for creating portable specifications of real world systems. During the last few years, I have been working on a tool called ADATT. This tool focuses on being comfortably usable by domain experts (poster, talk, current status).
In 2017 I gave a master course on Interactive Theorem Proving at KTH focusing on HOL 4. The slides (printer-friendly version, Latex sources) as well as the exercise sheets are available online.
A list of my publications, talks und similar documents can be found on my personal webpage.
As part of a commercial formal methods team I helped hardening a microhypervisor using Coq between July 2014 and September 2016.
The following information (Impressum) is required under German law. This page is also available in German.
Dr. Thomas Tuerk, Dipl.-Inf.
IT Consulting and services: system development and maintenance, consulting and trainings for companies and individuals, main focus on formal methods and interactive theorem proving
|Address||Dr. Thomas Tuerk|
|phone||+49 6483 803150|
|VAT Reg No||DE350366445|
Personal data (usually referred to just as data below) will only be processed by us to the extent necessary and for the purpose of providing a functional and user-friendly website, including its contents, and the services offered there.
Per Art. 4 No. 1 of Regulation (EU) 2016/679, i.e. the General Data Protection Regulation (hereinafter referred to as the GDPR), processing refers to any operation or set of operations such as collection, recording, organization, structuring, storage, adaptation, alteration, retrieval, consultation, use, disclosure by transmission, dissemination, or otherwise making available, alignment, or combination, restriction, erasure, or destruction performed on personal data, whether by automated means or not.
I. Information about us as controllers of your data
II. The rights of users and data subjects
III. Information about the data processing
The party responsible for this website (the controller) for purposes of data protection law is:
phone: +49 6483 803150
With regard to the data processing to be described in more detail below, users and data subjects have the right
In addition, the controller is obliged to inform all recipients to whom it discloses data of any such corrections, deletions, or restrictions placed on processing the same per Art. 16, 17 Para. 1, 18 GDPR. However, this obligation does not apply if such notification is impossible or involves a disproportionate effort. Nevertheless, users have a right to information about these recipients.
Likewise, under Art. 21 GDPR, users and data subjects have the right to object to the controller's future processing of their data pursuant to Art. 6 Para. 1 lit. f) GDPR. In particular, an objection to data processing for the purpose of direct advertising is permissible.
Your data processed when using our website will be deleted or blocked as soon as the purpose for its storage ceases to apply, provided the deletion of the same is not in breach of any statutory storage obligations or unless otherwise stipulated below.
For technical reasons, the following data sent by your internet browser to us or to our server provider will be collected, especially to ensure a secure and stable website: These server log files record the type and version of your browser, operating system, the website from which you came (referrer URL), the webpages on our site visited, the date and time of your visit, as well as the IP address from which you visited our site.
The data thus collected will be temporarily stored, but not in association with any other of your data.
The basis for this storage is Art. 6 Para. 1 lit. f) GDPR. Our legitimate interest lies in the improvement, stability, functionality, and security of our website.
The data will be deleted within no more than seven days, unless continued storage is required for evidentiary purposes. In which case, all or part of the data will be excluded from deletion until the investigation of the relevant incident is finally resolved.
This processing makes our website more user-friendly, efficient, and secure. A cookie is for example used to enable then the login into the ticket-system.
The legal basis for such processing is Art. 6 Para. 1 lit. f) GDPR. Our legitimate interest lies in improving the functionality of our website.
If you prevent or restrict the installation of cookies, not all of the functions on our site may be fully usable.
If you contact us (e.g. via email or the ticket-system), the data you provide will be used for the purpose of processing your request. We must have this data in order to process and answer your inquiry; otherwise we will not be able to answer it in full or at all.
The legal basis for this data processing is Art. 6 Para. 1 lit. b) GDPR.
Your data (with exception to the data entered into the ticket-system) will be deleted once we have fully answered your inquiry and there is no further legal obligation to store your data, such as if an order or contract resulted therefrom. The data in the ticket-system will be stored until you ask us to delete it. This allows you to access you old requests.
based on Model Data Protection Statement by Anwaltskanzlei Weiß & Partner