IT-Dienstleistungen Dr. Thomas Türk Sprache wechseln en
Dr. Thomas Türk
Dr. Thomas Türk
Experte für interaktives Theorembeweisen

Ich biete als Freiberufler IT-Dienstleistungen und IT-Beratung. Unter anderem biete ich Systementwicklung und -instandhaltung sowie Beratung und Schulungen für Unternehmen sowie Privatpersonen an. Mein Schwerpunkt liegt bei formalen Methoden und interaktivem Theorembeweisen, ich arbeite jedoch auch in anderen Bereichen.

Fähigkeiten

Sprachkenntnisse

Deutsch (Muttersprache), Englisch (verhandlungssicher)

Programmiersprachen

Haskell, OCaml, SML, Python, Java, C#, Javascript, C++, Bash-Scripte, Perl, PHP, ...

weitere IT-Kenntnisse

Datenbankentwicklung (besonders MySQL und MS SQL Server), Git, XML, HTML, CSS, JSON, Docker, ...

Theorembeweisen

Experte für den HOL 4 theorem prover, erfahrener Nutzer von Isabelle/HOL und Coq

Spezifikation und Conformance Testing

Erfahrung mit Model based Testing; einer der Entwickler von Lem; Entwickler von ADATT; Mitarbeit an Spezifikation von POSIX Dateisystemen

Hardwarenahe Entwicklung

Erfahrung mit Verifikation hardwarenahen Codes, z.B. Verifikation eines Microhypervisors oder eines Transpiler für Binärcode; Erfahrung mit Temporallogiken und Model-Checking

Program Refinement

Mitarbeit an Program Refinement Framework in Isabelle/HOL; Entwurf eines einfachen Pragram Refinement Frameworks in Coq genutzt für Verifikation eines Micro-Hypervisors

Lehre

in Lehre an Universitäten involviert; zuletzt Master-Course über Theorembeweisen an der Königlich Technischen Hochschule in Stockholm (Folien)

Curriculum Vitae

Berufserfahrung

Juli 2025 - ...

Geschäftsführer Thomas Tuerk GmbH, Thomas Tuerk GmbH, Brechen, Deutschland.

die Thomas Tuerk GmbH entwickelt und vertreibt Software

Jan. 2022 - ...

Freiberufler, IT Dienstleistungen Dr. Thomas Türk, Brechen, Deutschland.

Mai 2021 - Okt. 2021

Entwickler, F+S Fleckner und Simon Informationstechnik GmbH, Limburg, Deutschland.

Nov. 2017 - April 2021

Entwickler, et-systems GmbH, Limburg, Deutschland.

Entwickler für kundenspezifische Anpassungen am ERP System APplus, 20 h pro Woche, Webentwicklung (Javacript, CSS, HTML) in ASP.NET (vor allem C#) mit Java Application Server und Microsoft SQL Server

Nov. 2017 - April 2021

Independent Scholar, Brechen, Deutschland.

Entwicklung von ADATT, eines Tools für das Schreiben formaler Spezifikationen

April 2017 - Okt. 2017

Postdoktor, KTH, Stockholm, Schweden.

Mitarbeit im PROSPER Projekt, Lehre besonders in Bezug auf Theorembeweiser HOL, Arbeit an verifiziertem Transpiler von Binärcode in Maschinen-unabhängige Repräsentation

Juli 2014 - Sep. 2016

Formal Methods Staff Engineer, FireEye, Dresden, Deutschland.

Verifizierung eines Micro-Hypervisors, Program Refinement, Erstellung eines Coq Models und dazugehöriger Beweise sowie Conformance Testing, Administration der Test-Server

Jan. 2014 - Juli 2014

Computer Science Engineer, University of Leicester, Leicester, Vereinigtes Königreich.

Arbeit mit Dr. Tom Ridge am The future filesystems project Projekt, Mitarbeit bei Formalisierung von POSIX Dateisystemen in Lem sowie beim Testen dieser Formalisierung

Juli 2012 - Jan. 2014

Research Associate, University of Cambridge, Cambridge, Vereinigtes Königreich.

Arbeit mit Prof. Peter Sewell am Projekt Rigorous Engineering for Mainstream Systems, insbesondere Entwicklung des Tools Lem

Mai 2011 - Juli 2012

Wissenschaftlicher Mitarbeiter, TU München, München, Deutschland.

Arbeit mit Prof. Tobias Nipkow am CAVA Projekt

Jan. 2010 - Jan. 2011

Research Assistant, University of Cambridge, Cambridge, Vereinigtes Königreich.

Teilzeitarbeit für Dr. Parkinson am Separation Logic Tool JStar während des Schreibens meiner Doktorarbeit

Ausbildung

Nov. 2002 - April 2011

Ph.D., University of Cambridge, Cambridge, Vereinigtes Königreich.

Beginn im PhD Programm der TU Kaiserslautern parallel mit Diplomstudiengang; als Teil dieses Programms Besuch in Cambridge Januar - Juni 2006; Abbruch in Kaiserslautern und Beginn eines PhD Studiums in Cambridge Jan. 2007; Betreuer Prof. Mike Gordon; Dissertationsthema A Separation Logic Framework for HOL

Okt. 1999 - Mai 2005

Diplom, TU Kaiserslautern, Kaiserslautern, Deutschland.

Schwerpunkt Formale Methoden, Diplomarbeit A Hierarchy for Accellera's Property Specification Language betreut von Prof. K. Schneider, Note 1,2

1990 - 1999

Abitur, Tilemannschule Limburg, Limburg, Deutschland.

Leistungfächer Chemie, Mathematik, Note 1,0

Kontakt

Foto Thomas Türk

Dr. Thomas Türk
Albert-Otto-Str. 8
65611 Brechen
Deutschland
Telefon+49 6483 803150
eMailkontakt@thomas-tuerk.de
Helpdeskhttps://helpdesk.thomas-tuerk.de


Sollte ich Ihr Interesse geweckt haben, kontaktieren Sie mich doch unverbindlich. Dafür bietet sich eine eMail oder ein Telefonanruf an. Nach initialer Kontaktaufnahme stehe ich Ihnen auch gerne für persönliche Treffen und über andere Kommunikationswege (z.B. übliche Videotelefonieplattformen) zur Verfügung. Für bestehende Kunden kann, insbesondere im Zusammenhang mit bestehenden Aufträgen, auch die Verwendung meines Helpdesks sinnvoll sein.

Eine Liste meiner Veröffentlichungen, Vorträge und sonstiger Dokumente finden Sie unter Veröffentlichungen.

Hier finden Sie eine Auswahl meiner aktuellen und alten Projekte:

Lem / ADATT

Mein besonderes Interesse liegt in der Vereinfachung der Kommunikation zwischen Domain-Experten und Experten für interaktives Theorembeweisen (ITP). Um interaktiven Theorembeweisen (ITP) für die Absicherung praxisrelevanter Systeme einsetzen zu können, werden zuverlässige, detaillierte Modelle realer, großer System wie z.B. Prozessoren oder Programmiersprachen benötigt. Dies ist sehr viel Arbeit und die nötigen Details sind nur Experten für diese Systeme (im Folgenden Domain-Experten genannt) bekannt. Solche Domain-Experten sind jedoch meist keine Experten für formale Methoden oder ITP. Eine solche ITP Expertise ist jedoch für die Erstellung guter formaler Modelle nötig. Ich interessiere mich für die Zusammenarbeit von Domain- und ITP-Experten für bei der Erstellung solcher Modelle.

Mein Interesse erwachte bei der Arbeit Prof. Peter Sewell an Lem, einem Tool für die Erstellung portabler Spezifikationen. Die letzten Jahre habe ich in meiner Freizeit an einem Tools namens ADATT gearbeitet, dessen Schwerpunkt auf einfacher Benutzbarkeit durch Domain-Experten liegt. (Poster, Vortrag, aktueller Status). Aufgrund anderer Projekte fand in den letzten Jahren kaum Arbeit an ADATT statt. Ich plane aber weiterhin, daran weiterzuarbeiten.

Holfoot

Für meine Doktorarbeit (A Separation Logic Framework for HOL) habe ich das Tool Holfoot entwickelt, eine Formalisierung von Smallfoot im Theorembeweiser HOL 4. Holfoot ist online verfügbar (Poster, Paper TPHOLs 2009, Vortrag).

Vorlesung über interaktives Theorembeweisen

2017 gab ich eine Vorlesung über iteraktives Theorembeweisen und den Theorembeweiser HOL 4 an der KTH in Stockholm. Die von mir für diese Vorlesung in englischer Sprache erstellten Folien (Druckversion, Quellen) sowie die Übungsblätter sind frei verfügbar.

Verifikation eines Micro-Hypervisor mit Coq

Als Teil eines kommerziellen Formalen-Methoden-Teams arbeitete ich zwischen Juli 2014 und Sep. 2016 an der Absicherung eines Micro-Hypersors mit Hilfe von Coq.

Die meisten meiner Veröffentlichungen, Vorträge und sonstigen Dokumente sind in englischer Sprache verfasst.

Veröffentlichungen

2016

Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor

Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, Cesar Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk

FM 2016

2015

Pattern Matches in HOL: A New Representation and Improved Code Generation

T. Tuerk and M. Myreen and R. Kumar

ITP 2015

2015

SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems

Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, Peter Sewell

SOSP 2015

2012

Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm

P. Lammich and T. Tuerk

ITP 2012

2011

A Separation Logic Framework for HOL

T. Tuerk

PhD thesis, Technical Report

2010

Local Reasoning about While-Loops

T. Tuerk

Verified Software: Theories, Tools and Experiments 2010 - Theory Workshop

2009

A formalisation of Smallfoot in HOL

T. Tuerk

Theorem Proving in Higher Order Logics (TPHOLs)

2008

A Separation Logic Framework in HOL

T. Tuerk

Theorem Proving in Higher Order Logics (TPHOLs) : Emerging Trends

2007

Model Checking PSL Using HOL and SMV

T. Tuerk and K. Schneider and M. Gordon

Haifa Verification Conference (HVC)

2005

Improving Constructiveness in Code Generators

K. Schneider and J. Brandt and T. Schuele and T. Tuerk

Synchronous Languages, Applications, and Programming (SLAP)

2005

Maximal Causality Analysis

K. Schneider and J. Brandt and T. Schuele and T. Tuerk

Application of Concurrency to System Design (ACSD)

2005

From PSL to LTL: A Formal Validation in HOL

T. Tuerk and K. Schneider

Theorem Proving in Higher Order Logic (TPHOL)

2005

Relationship between Alternating omega-Automata and Symbolically Represented Nondeterministic omega-Automata

T. Tuerk and K. Schneider

Technical Report

2005

A Hierarchy for Accellera's Property Specification Language

T. Tuerk

Master Thesis

Vorträge

13 April 2018

ARW 2018

Real-world formal documentation

24 Aug. 2015

ITP 2015

Pattern Matches in HOL: A New Representation and Improved Code Generation

13 Aug. 2012

ITP 2012

Applying Data Refinement for Monadic Programs to Hopcroft's Algorithm

29 Feb. 2012

Club2

A Formalisation of Finite Automata in Isabelle/HOL

1 Feb. 2011

ARG Lunch

Quantifier Heurististics in HOL4

18 Aug. 2010

VSTTE'10 - Theory Workshop

Local Reasoning about While-Loops

26 Jan. 2010

ARG Lunch

A demo of Holfoot

24 Nov. 2009

ARG Lunch

A presentation of some tools used for Holfoot

19 Aug. 2009

TPHOLs

A formalisation of Smallfoot in HOL

5 May 2009

ARG Lunch

A Heap of Problems

27 Jan. 2009

ARG Lunch

A HOL implementation of Smallfoot

2 Sep. 2008

Research & review meeting

A fully-expansive HOL implementation of Smallfoot

19 Feb. 2008

ARG Lunch

An Embedding of Abstract Separation Logic in HOL

26 Jun. 2007

ARG Lunch

A Deep Embedding of a Decidable Fragment of Separation Logic in HOL

7 Nov. 2006

ARG Lunch

A verifying ARM compiler

23 Oct. 2006

Haifa Verification Conference

Model Checking PSL using HOL and SMV

21 Jun. 2006

ARG Lunch

Deep Embeddings of Temporal Logics in HOL

1 Feb. 2006

ARG Lunch

PSL in HolCheck

23 Aug. 2005

TPHOLs

From PSL to LTL: A Formal Validation in HOL

Poster

Adatt

A Heap of Problems

PSL

Sonstige Dokumente

2017

Slides of HOL master course

T. Tuerk

given at KTH in 2017

2012

Documentation of the HOL 4 quantifier elimination library

T. Tuerk

distributed together with HOL 4 in directory src/quantHeuristics/doc

Ältere deutschsprachige Dokumente

2003

Constraintbasierte Vervollständigungstechniken: Gleichheitsconstraints

T. Tuerk

Projektarbeit

1997

Qumran

T. Tuerk

ein Schulreferat

Impressum

Angaben gemäß § 5 DDG

Dr. Thomas Türk, Dipl.-Inf.

IT Beratung und Dienstleistungen: Systementwicklung und -instandhaltung, Beratung und Schulungen für Unternehmen sowie Privatpersonen, Schwerpunkt formale Methoden und interaktives Theorembeweisen

Adresse Dr. Thomas Türk
Albert-Otto-Str. 8
65611 Brechen
Deutschland
Telefon+49 6483 803150
+44 1223 858866
eMailkontakt@thomas-tuerk.de
Umsatzsteuer-IDDE350366445


Verantwortlich für den Inhalt

Dr. Thomas Türk, Albert-Otto-Str. 8, 65611 Brechen

Bildnachweis

Datenschutzerklärung

Personenbezogene Daten (nachfolgend zumeist nur Daten genannt) werden von uns nur im Rahmen der Erforderlichkeit sowie zum Zwecke der Bereitstellung eines funktionsfähigen und nutzerfreundlichen Internetauftritts, inklusive seiner Inhalte und der dort angebotenen Leistungen, verarbeitet.

Gemäß Art. 4 Nr. 2 der Verordnung (EU) 2016/679, also der Datenschutz-Grundverordnung (nachfolgend nur DSGVO genannt), gilt als Verarbeitung jeder mit oder ohne Hilfe automatisierter Verfahren ausgeführter Vorgang oder jede solche Vorgangsreihe im Zusammenhang mit personenbezogenen Daten, wie das Erheben, das Erfassen, die Organisation, das Ordnen, die Speicherung, die Anpassung oder Veränderung, das Auslesen, das Abfragen, die Verwendung, die Offenlegung durch Übermittlung, Verbreitung oder eine andere Form der Bereitstellung, den Abgleich oder die Verknüpfung, die Einschränkung, das Löschen oder die Vernichtung.

Mit der nachfolgenden Datenschutzerklärung informieren wir Sie insbesondere über Art, Umfang, Zweck, Dauer und Rechtsgrundlage der Verarbeitung personenbezogener Daten, soweit wir entweder allein oder gemeinsam mit anderen über die Zwecke und Mittel der Verarbeitung entscheiden.

Unsere Datenschutzerklärung ist wie folgt gegliedert:

I. Informationen über uns als Verantwortliche
II. Rechte der Nutzer und Betroffenen
III. Informationen zur Datenverarbeitung

I. Informationen über uns als Verantwortliche

Verantwortlicher Anbieter dieses Internetauftritts im datenschutzrechtlichen Sinne ist:

Thomas Türk
Albert-Otto-Str. 8
65611 Brechen
Deutschland

Telefon: +49 6483 803150
E-Mail: kontakt@thomas-tuerk.de

II. Rechte der Nutzer und Betroffenen

Mit Blick auf die nachfolgend noch näher beschriebene Datenverarbeitung haben die Nutzer und Betroffenen das Recht

  • auf Bestätigung, ob sie betreffende Daten verarbeitet werden, auf Auskunft über die verarbeiteten Daten, auf weitere Informationen über die Datenverarbeitung sowie auf Kopien der Daten (vgl. auch Art. 15 DSGVO);
  • auf Berichtigung oder Vervollständigung unrichtiger bzw. unvollständiger Daten (vgl. auch Art. 16 DSGVO);
  • auf unverzügliche Löschung der sie betreffenden Daten (vgl. auch Art. 17 DSGVO), oder, alternativ, soweit eine weitere Verarbeitung gemäß Art. 17 Abs. 3 DSGVO erforderlich ist, auf Einschränkung der Verarbeitung nach Maßgabe von Art. 18 DSGVO;
  • auf Erhalt der sie betreffenden und von ihnen bereitgestellten Daten und auf Übermittlung dieser Daten an andere Anbieter/Verantwortliche (vgl. auch Art. 20 DSGVO);
  • auf Beschwerde gegenüber der Aufsichtsbehörde, sofern sie der Ansicht sind, dass die sie betreffenden Daten durch den Anbieter unter Verstoß gegen datenschutzrechtliche Bestimmungen verarbeitet werden (vgl. auch Art. 77 DSGVO).

Darüber hinaus ist der Anbieter dazu verpflichtet, alle Empfänger, denen gegenüber Daten durch den Anbieter offengelegt worden sind, über jedwede Berichtigung oder Löschung von Daten oder die Einschränkung der Verarbeitung, die aufgrund der Artikel 16, 17 Abs. 1, 18 DSGVO erfolgt, zu unterrichten. Diese Verpflichtung besteht jedoch nicht, soweit diese Mitteilung unmöglich oder mit einem unverhältnismäßigen Aufwand verbunden ist. Unbeschadet dessen hat der Nutzer ein Recht auf Auskunft über diese Empfänger.

Ebenfalls haben die Nutzer und Betroffenen nach Art. 21 DSGVO das Recht auf Widerspruch gegen die künftige Verarbeitung der sie betreffenden Daten, sofern die Daten durch den Anbieter nach Maßgabe von Art. 6 Abs. 1 lit. f) DSGVO verarbeitet werden. Insbesondere ist ein Widerspruch gegen die Datenverarbeitung zum Zwecke der Direktwerbung statthaft.

III. Informationen zur Datenverarbeitung

Ihre bei Nutzung unseres Internetauftritts verarbeiteten Daten werden gelöscht oder gesperrt, sobald der Zweck der Speicherung entfällt, der Löschung der Daten keine gesetzlichen Aufbewahrungspflichten entgegenstehen und nachfolgend keine anderslautenden Angaben zu einzelnen Verarbeitungsverfahren gemacht werden.

Serverdaten

Aus technischen Gründen, insbesondere zur Gewährleistung eines sicheren und stabilen Internetauftritts, werden Daten durch Ihren Internet-Browser an unseren Server übermittelt. Mit diesen sog. Server-Logfiles werden u.a. Typ und Version Ihres Internetbrowsers, das Betriebssystem, die Website, von der aus Sie auf unseren Internetauftritt gewechselt haben (Referrer URL), die Website(s) unseres Internetauftritts, die Sie besuchen, Datum und Uhrzeit des jeweiligen Zugriffs sowie die IP-Adresse des Internetanschlusses, von dem aus die Nutzung unseres Internetauftritts erfolgt, erhoben.

Diese so erhobenen Daten werden vorübergehend gespeichert, dies jedoch nicht gemeinsam mit anderen Daten von Ihnen.

Diese Speicherung erfolgt auf der Rechtsgrundlage von Art. 6 Abs. 1 lit. f) DSGVO. Unser berechtigtes Interesse liegt in der Verbesserung, Stabilität, Funktionalität und Sicherheit unseres Internetauftritts.

Die Daten werden spätestens nach sieben Tagen wieder gelöscht, soweit keine weitere Aufbewahrung zu Beweiszwecken erforderlich ist. Andernfalls sind die Daten bis zur endgültigen Klärung eines Vorfalls ganz oder teilweise von der Löschung ausgenommen.

Cookies

a) Einsatz von Cookies

Diese Website (https://www.thomas-tuerk.de) verwendet keine Cookies. Cookies werden aber von unserem Ticketsystem (https://helpdesk.thomas-tuerk.de), unserem Nextcloud-Server (https://nextcloud.thomas-tuerk.de) sowie dem Git-Server (https://git.thomas-tuerk.de) eingesetzt, teilweise auch ohne Anmeldung. Cookies sind kleine Textdateien oder andere Speichertechnologien, die durch den von Ihnen eingesetzten Internet-Browser auf Ihrem Endgerät abgelegt und gespeichert werden. Durch diese Cookies werden im individuellen Umfang bestimmte Informationen von Ihnen, wie beispielsweise Ihre Browser- oder Standortdaten oder Ihre IP-Adresse, verarbeitet.

Durch diese Verarbeitung werden unsere Dienste benutzerfreundlicher, effektiver und sicherer. Ein Cookie ermöglicht beispielsweise den Login in unser Ticketsystem.

Rechtsgrundlage dieser Verarbeitung ist Art. 6 Abs. 1 lit. f) DSGVO. Unser berechtigtes Interesse liegt in der Verbesserung der Funktionalität dieser Dienste.

b) Beseitigungsmöglichkeit

Sie können die Installation der Cookies durch eine Einstellung Ihres Internet-Browsers verhindern oder einschränken. Ebenfalls können Sie bereits gespeicherte Cookies jederzeit löschen. Die hierfür erforderlichen Schritte und Maßnahmen hängen jedoch von Ihrem konkret genutzten Internet-Browser ab. Bei Fragen benutzen Sie daher bitte die Hilfefunktion oder Dokumentation Ihres Internet-Browsers oder wenden sich an dessen Hersteller bzw. Support.

Sollten Sie die Installation der Cookies verhindern oder einschränken, kann dies allerdings dazu führen, dass nicht sämtliche Funktionen dieser Dienste vollumfänglich nutzbar sind.

Kontaktanfragen, Ticketsystem, Nextcloud und Git-Server

Sofern Sie per E-Mail oder über unser Ticketsystem (https://helpdesk.thomas-tuerk.de) mit uns in Kontakt treten, werden die dabei von Ihnen angegebenen Daten zur Bearbeitung Ihrer Anfrage genutzt. Die Angabe der Daten ist zur Bearbeitung und Beantwortung Ihrer Anfrage erforderlich - ohne deren Bereitstellung können wir Ihre Anfrage nicht oder allenfalls eingeschränkt beantworten. Anfragen über das Ticketsystem sind auch ohne Benutzerkonto möglich.

Für die Zusammenarbeit mit Kunden und Projektpartnern betreiben wir zusätzlich einen Nextcloud-Server (https://nextcloud.thomas-tuerk.de) zum Austausch von Dateien sowie einen Git-Server (https://git.thomas-tuerk.de) zur Verwaltung von Quellcode. Ticketsystem, Nextcloud und Git-Server werden, ebenso wie diese Website, auf einem von uns selbst administrierten dedizierten Server betrieben. Dieser ist bei der Hetzner Online GmbH, Industriestr. 25, 91710 Gunzenhausen, angemietet und steht in deren Rechenzentrum in Falkenstein (Deutschland). Mit Hetzner besteht ein Vertrag zur Auftragsverarbeitung gemäß Art. 28 DSGVO. Eine darüber hinausgehende Weitergabe der dort gespeicherten Daten an Dritte findet nicht statt.

Sofern Sie ein Benutzerkonto für einen dieser Dienste nutzen, verarbeiten wir Ihren Namen, Ihre E-Mail-Adresse und Ihren Benutzernamen sowie die von Ihnen eingestellten Inhalte (z.B. Anfragen, Dateien, Quellcode, Kommentare) und zugehörige Metadaten wie Zeitpunkt und Urheber von Änderungen.

In der Nextcloud und auf dem Git-Server gibt es zudem öffentlich freigegebene Inhalte, etwa öffentliche Repositories oder Freigabe-Links. Diese können ohne Benutzerkonto abgerufen werden. Dabei werden die oben unter „Serverdaten“ beschriebenen Server-Logfiles erhoben; zudem können die Dienste auch ohne Anmeldung technisch notwendige Cookies setzen (siehe „Cookies“).

Rechtsgrundlage für diese Verarbeitung ist Art. 6 Abs. 1 lit. b) DSGVO, soweit sie der Durchführung eines Vertrags oder vorvertraglicher Maßnahmen dient, im Übrigen Art. 6 Abs. 1 lit. f) DSGVO. Unser berechtigtes Interesse liegt in der Beantwortung von Anfragen sowie einer effizienten und sicheren Zusammenarbeit.

Daten aus Anfragen per E-Mail werden gelöscht, sofern Ihre Anfrage abschließend beantwortet worden ist und der Löschung keine gesetzlichen Aufbewahrungspflichten entgegenstehen, wie bspw. bei einer sich etwaig anschließenden Vertragsabwicklung. Ihre Daten im Ticketsystem, in der Nextcloud und auf dem Git-Server werden gespeichert, bis Sie uns zur Löschung auffordern. Dadurch ist es Ihnen beispielsweise möglich zu sehen, welche Anfragen Sie uns bereits gestellt haben. Inhalte in Git-Repositories sind Teil der Versionsgeschichte; ihre Löschung erfolgt daher in der Regel durch Löschen des gesamten Repositories.

Basierend auf Muster-Datenschutzerklärung der Anwaltskanzlei Weiß & Partner.

Advanced Documentation And Testing Tool

I'm currently developing a tool for advanced testing and documentation in my spare time. This is still work in progress. However, here some preliminary information can already been found. If you are interested in learning details or even in playing around with very early, unfinished versions, please feel free to contact me.

Presentation at ARW 2018

Some talk and corresponding short abstract from early stages in April 2018 are available.

Very high level description

Advanced Documentation and Testing Tool (Adatt) is a tool for writing formal, executable specifications. It is intended to be used by both domain and formal-method experts. Different users with different backgrounds can contribute different parts of a specification. One core idea is using the same Adatt documents for multiple purposes and allowing different users with different backgrounds to contribute to different parts of a specification.

Superficially, Adatt looks like a functional programming language with special support for writing documentation and specifications. Once finished, one will be able to translate Adatt specifications to

  • high quality human readable documentation (Latex, HTML)
  • executable code (Ocaml, SML, Haskell, Javascript, ...)
  • formal specifications for interactive theorem provers (HOL 4, Isabelle/HOL, Coq)

One will be able to start with writing human readable documentation without any formal content. Declaring types or constants (including functions), which are referred to in the natural language text, can improve the documentation by e.g. ensuring there are no spelling mistakes. The documentation can be further improved by adding some type definitions, constant signatures or simple test-cases.

At this stage, the documention / specification is perhaps already detailed enough to generate little bits of executable code or at least code stubs. Such code can be used e.g. for test-oracles. By adding more test cases and simple executable specifications the generated executable code becomes more complete and thereby useful.

Even if not all types and constants are defined yet, one can already use formal methods to reason about the existing specifications and test-cases. However, by adding non-executable properties and by asking theorem prover experts to add more complicated specifications in the end a good formal specification can be written that maps well to theories already present in various interactive theorem provers.

Current Status (May 2021)

The main language of Adatt and its typechecking are finished. Specifications that look similar to a functional program can be written in this language, parsed and checked. There is a Language Server Protocol server for Adatt and a Visual Studio Code plugin using this server. While editing files, only the affected parts of the currently opened files are (re)-typechecked. Unaffected parts already typechecked are just kept. Together with a concurrent implementation that can use multiple cores effectively, this leads to very rapid feedback (usually within a few milliseconds).

Typechecking might sound like a very early stage. Notice however, that in constrast to nearly all compilers for programming languages, Adatt outputs results at the same level of abstraction as the input. Therefore, mst of the work that needs to be performed by Adatt is already performed during the typechecking stage. This includes:

  • pattern compilation, in particular
    • checking whether pattern matches are complete
    • find overlapping or redundant patterns
    • automatically add missing cases
  • resolving of type-class intances
  • a built-in template language for generating Adatt code based on e.g. type definitions
    • mainly used for automatically generating type-class instances
    • also used for generating recognizers and lenses
    • intended to be used later for backends as well
  • producing auxiliary information about the analysed code
    • annotations like the type of locally used variables
    • automatic code fixes (i.e. automatic edits like adding a declaration of a constant)
    • links like jumping from an usage point to the definition point of a constant
  • enforce user-configurable code styles
    • naming conventions
    • detection of similar and therefore potentially problematic names for different concepts
  • build-up detailled internal datastructures suitable for producing output later

The output needs to be highly configurable. For human readable output like html, the preferred style depends a lot on the intended usage and also personal taste. For output of executable code, programming languages and especially libraries evolve over time. Moreover, if the generated code is used by hand-written code, fine tuning the generated code might be very useful to ease usage and integrating in existing code-bases. These same issues also exist for interactive theorem provers. In this (as in many other) respect they are similar to programming languages.

To provide this needed flexibility, the output is generated by user-changeable LUA-scripts. The simplest case is the output of human readable documentation. In this simple case, Adatt loads a project and executes user-written LUA scripts in this context of this project. There are commands for typechecking files and modules available. One can check for errors and warnings and report these. One can also get information about the checked files and modules. This includes information like the list of seen files or modules, the constants, types, type-classes etc. One can access information like where a constant is defined or used or which instances are known for a type-class. Most importantly, one can access the input (both whole files and just parts) enriched with annotations collected during type-checking. This enriched input is the main source for generating human readable output. Adatt comes with specialised LUA libraries which allow to easily access all this functionality of Adatt. Moreover, there are example LUA scripts that use this libray to e.g. generate HTML output. These example scripts an be used as they are or as a template for writing own LUA-scripts.

The support for generating human readable output is essentially finished. A few convenience functions could still be added and the output tuned a bit, but the main functionality is all there.

Outputting executable code or specifications is more difficult and unluckily still work in progress. For these cases, information needs to be passed from LUA to Adatt when processing a project. It should be possible to e.g. state inside an Adatt module, how to output a given Adatt constant for a given backend. This can be specified using Adatt's template language. More interesting, it should be possible to add backend-specific annotations. For example, most theorem proving backends need to prove that recursive constants are well-defined (which in practice is very similar to a termination argument) while defining such constants. A backend-specific annotation might either state that some built-in termination-proof-method should be tried or provide a termination argument manually. It should be possible to add such backend-specific annotations in Adatt files next to the definition of the recursive constant. To support this, Lua-written backends need to pass information to Adatt before even parsing files.

Another complication is that programming language and theorem prover backends need to be able to ask Adatt to perform inlining, (partial) pattern compilation and other code-operations. Thus, these backends require much more infrastructure than human readable documentation ones. Currently, I'm working on implementing this infrastructure.

Rough plan for next steps

  • continue implementing infrastructure for theorem proving and programming language backends
  • implement SML, HOL and Coq backends
  • add annotations to Adatt library for mapping Adatt definitions to commonly used backend libraries
  • play around with some small, very simple examples
  • consider releasing a very first, alpha version of Adatt
  • implement some bigger, more interesting example
  • add further backends (Isabelle/HOL, OCaml, Haskell, Java-Script, ...)
  • drastically improve support for writing natural language documentation
    • more work on comments in Adatt, e.g.
      • links to Adatt entities
      • allow subset of markdown in comments
      • allow special comments with Latex contents
      • like Haddock associate certain comments with types, constants, fields, arguments, ...
    • add additional input file format which supports some kind of literal programming style
  • add additional features like perhaps
    • inductive relations
    • type-invariants
    • indexed types
    • ...

Some documents

So far, I have been pretty lazy writing documentation. Here are some notes describing mostly some language features and the reasoning behind them. This needs a lot(!) of work before one can even think of calling it documentation. Nevertheless, it might already provide a rough idea about Adatt. For the same reason, the pretty-printed library of Adatt is provided. The pretty-printing is done using Adatt itself via a LUA-written HTML and Latex backends. Adatt's library still needs lots of work. However, it already provides an impression, how Adatt code looks like.