Dr. Thomas Tuerk
Interactive theorem proving expert

As a freelancer I offer system development and maintenance as well as consulting and training for companies and individuals. My focus is on formal methods, especially interactive theorem proving.

Skills

Curriculum Vitae

Work Experience

Education

Contact Details

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.

A list of my publications, talks and other documents is available under Publications.

Here you can find some selected projects of mine:

Lem / ADATT

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).

Holfoot

As part of my PhD (A Separation Logic Framework for HOL) I developed the tool Holfoot, a formalisation of Smallfoot in the HOL 4 theorem prover. Holfoot is available online (poster, TPHOLs 2009 paper, talk).

Master Course on Interactive Theorem Proving

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.

Hardening a microhypervisor using Coq in industry

As part of a commercial formal methods team I helped hardening a microhypervisor using Coq between July 2014 and September 2016.

Impressum - Legal Notifications

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

Picture Credits

• The background image of this page is by Monica Sauro, it has been published at Unsplash.
• This webpage uses the CMS Grav with a heavily modified version of the personal theme by Mohamed Safouan Besrour
• The icon-pack (license CC BY 4.0) by keyamoon is used.
• flag symbols
  • UK: Original: Acts of Union 1800 Vector: Zscout370, Public domain, via Wikimedia Commons
  • DE: User:SKopp, User:Madden, and other users, Public domain, via Wikimedia Commons

Privacy Policy

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. 2 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.

The following privacy policy is intended to inform you in particular about the type, scope, purpose, duration, and legal basis for the processing of such data either under our own control or in conjunction with others.

Our privacy policy is structured as follows:

I. Information about us as controllers of your data
II. The rights of users and data subjects
III. Information about the data processing

I. Information about us as controllers of your data

The party responsible for this website (the controller) for purposes of data protection law is:

Thomas Tuerk
Albert-Otto-Str. 8
65611 Brechen
Germany

phone: +49 6483 803150
email: kontakt@thomas-tuerk.de

II. The rights of users and data subjects

With regard to the data processing to be described in more detail below, users and data subjects have the right

• to confirmation of whether data concerning them is being processed, information about the data being processed, further information about the nature of the data processing, and copies of the data (cf. also Art. 15 GDPR);
• to correct or complete incorrect or incomplete data (cf. also Art. 16 GDPR);
• to the immediate deletion of data concerning them (cf. also Art. 17 GDPR), or, alternatively, if further processing is necessary as stipulated in Art. 17 Para. 3 GDPR, to restrict said processing per Art. 18 GDPR;
• to receive copies of the data concerning them and/or provided by them and to have the same transmitted to other providers/controllers (cf. also Art. 20 GDPR);
• to file complaints with the supervisory authority if they believe that data concerning them is being processed by the controller in breach of data protection provisions (see also Art. 77 GDPR).

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.

III. Information about the data processing

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.

Server data

For technical reasons, the following data sent by your internet browser to our server 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.

Cookies

a) Use of cookies

This website (https://www.thomas-tuerk.de) does not use cookies. However, cookies are used by our ticket system (https://helpdesk.thomas-tuerk.de), our Nextcloud server (https://nextcloud.thomas-tuerk.de) and our Git server (https://git.thomas-tuerk.de), in some cases even without login. Cookies are small text files or other storage technologies stored on your device by your browser. These cookies process certain specific information about you, such as your browser, location data, or IP address.

This processing makes our services more user-friendly, efficient, and secure. A cookie is for example used to enable the login into our 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 these services.

b) Disabling cookies

You can refuse the use of cookies by changing the settings on your browser. Likewise, you can use the browser to delete cookies that have already been stored. However, the steps and measures required vary, depending on the browser you use. If you have any questions, please use the help function or consult the documentation for your browser or contact its maker for support.

If you prevent or restrict the installation of cookies, not all of the functions of these services may be fully usable.

Contact requests, ticket system, Nextcloud and Git server

If you contact us via email or our ticket system (https://helpdesk.thomas-tuerk.de), 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. Requests via the ticket system are also possible without a user account.

For collaboration with customers and project partners, we additionally operate a Nextcloud server (https://nextcloud.thomas-tuerk.de) for exchanging files and a Git server (https://git.thomas-tuerk.de) for managing source code. The ticket system, Nextcloud and Git server, as well as this website, are operated on a dedicated server administered by ourselves. This server is rented from Hetzner Online GmbH, Industriestr. 25, 91710 Gunzenhausen, Germany, and located in their data center in Falkenstein (Germany). A data processing agreement pursuant to Art. 28 GDPR has been concluded with Hetzner. Beyond this, the data stored there is not passed on to third parties.

If you use a user account for one of these services, we process your name, email address and user name as well as the content you provide (e.g. requests, files, source code, comments) and related metadata such as the time and author of changes.

Nextcloud and the Git server also contain publicly shared content, such as public repositories or share links. This content can be accessed without a user account. In this case, the server log files described above under "Server data" are collected; in addition, the services may set technically necessary cookies even without login (see "Cookies").

The legal basis for this processing is Art. 6 Para. 1 lit. b) GDPR insofar as it serves the performance of a contract or pre-contractual measures, and Art. 6 Para. 1 lit. f) GDPR otherwise. Our legitimate interest lies in answering requests and in efficient and secure collaboration.

Data from email requests 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. Your data in the ticket system, Nextcloud and the Git server will be stored until you ask us to delete it. This allows you, for example, to access your previous requests. Content in Git repositories is part of the version history; it is therefore usually deleted by deleting the entire repository.

based on Model Data Protection Statement by Anwaltskanzlei Weiß & Partner