• Interactive and automated theorem proving
• Software synthesis (frameworks)
• Proof visualiastion
• Usability in interactive theorem proving

Education

• Finished PhD studies in May 2024 for the academic degree "Dr. rer. nat." on the topic "On Synthesising Linux Kernel Module Components from Coq Formalisations"
• Finished the "Junior Teaching Professionals" Programme  of the Potsdam Graduate School in April 2015
• Degree "Dipl.-Inform" (Diploma in Computer Science) in June 2013 on the topic "TEMPLAR - Efficient Determination of Relevant Axioms in Big Formula Sets for Theorem Proving"

Scientific and Technical Positions

• Since 07/2024 - Research Associate (PostDoc),  Software Engineering Chair
• 04/2024-07/2024 - Research Assistant,  Software Engineering Chair
• 07/2021-03/2024 - Research Assistant, Theoretical Computer Science Chair (consortial project VERSECLOUD)
• 2016-2021 - Research Assistant, Theoretical Computer Science Chair
• 2014-2016 - Technical Assistant for the projects "Reisen.UP" and "Beschaffung.UP" at the CIO division, University of Potsdam

Frank, M. (2024): On Synthesising Linux Kernel Module Components from Coq Formalisations. Doctoral Thesis, University of Potsdam. published online at the Publication Server of the University of Potsdam, https://doi.org/10.25932/publishup-64255 (open access).

Repp, L.; Frank, M. (2024): nanoCoP-Ω: A Non-Clausal Connection Prover with Arithmetic. In: Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (Prague, Czech Republic, Sept. 18, 2023). Ed. by Jens Otten and Wolfgang Bibel. CEUR Workshop Proceedings 3613. Aachen, 2024, pp. 41–53.

Frinker, N.; Liebergeld, S.; Dr. Otto, A.; Frank, M.; Egger, M. (2023): Eine vertrauenswürdige, sichere Public Cloud - Utopie oder Realität. In: Digital sicher in eine nachhaltige Zukunft. 19. Deutscher IT-Sicherheitskongress. Bundesamt für Sicherheit in der Informationstechnik - BSI, 2023, pp. 227–240. ISBN: 978-3-922746-85-0.

Frinker, N.; Frank, M.; Liebergeld, S. (2023): VerSeCloud. Der Weg zur vertrauenswürdigen und sicheren Cloud "Made in Germany". In: Behörden Spiegel. Jahrgang. 39. Nr. 4 (2023), p. 31, ISSN: 1437-8337.

Kreitz, C.; Frank, M (2020): Automatische Inferenz. In: Handbuch der Künstlichen Intelligenz. Ed. by Günther Görz, Ute Schmid, and Tanya Braun. Berlin, Boston: De Gruyter, Dec. 16, 2020. Chap. 5, pp. 143–188. ISBN: 978-3-11-065984-9.

Frank, M (2020): The Coq Proof Script Visualiser (coq-psv). 11th Coq Workshop, colocated with IJCAR ’20. July 2020. Published as ePrint on arXiv.

Schellhorn, S.; Frank, M; Kreitz, C. (2019): Brückenkurse für mathematische und informatiknahe Studiengänge. In: Alles auf Anfang!. Ed. by Wilfried Schubarth, Sylvi Mauermeister, Friederike Schulze-Reichelt and Andreas Seidel. Potsdamer Beiträge zur Hochschulforschung, Heft 4 (2019). pp. 257-271. ISBN: 978-3-86956-452-4.

Frank, M.; Kreitz, C. (2018): A Theorem Prover for Scientific and Educational Purposes. EPTCS Vol. 267 (pp. 59-69).

Frank, M (2013/2014): TEMPLAR - Efficient Determination of Relevant Axioms in Big Formula Sets for Theorem Proving. Diploma Thesis, published 2014 online at the Institutional Repositoryof the University of Potsdam

Frank, M (2012/2014): ARDE - Technical Report. Student Work, published 2014 online at the Institutional Repository of the University of Potsdam

Frank, M. (2012): Relevanzbasiertes Preprocessing für automatische Theorembeweiser. In J. Schmidt, T. Riechert & S. Auer (ed.), SKIL 2012 - Dritte Studentenkonferenz Informatik Leipzig , Vol. 34 (pp. 87-98) . LIV . ISBN: 978-3-941608-21-4.

Further publications can be found under my ORCID profile.

Journal Reviews

Can be found on my ORCID profile

Artifact Evaluation

• Symposium on Principles of Programming Languages (POPL 2025)
• International Conference on Integrated Formal Methods (iFM 2023, iFM 2024)

Competitions

• Cade ATP Systems Competition (CASC-24), System: TEMPLAR::leanCoP
• Cade ATP Systems Competition (CASC-J6), System: leanCoP-ARDE

• ORCID
• DBLP
• ResearchGate
• Google Scholar
• Deutsche Nationalbibliothek
• PGP 0A98 A9ED 65D1 A1BB FB88 D69A 6D1B B85D 6DEE 684B

Masters Theses (As Co-Supervisor)

• Kranz, T. : "Induction Provers in Hets: Leveraging the Tons of Inductive Problems language and tools to talk to more Automated Theorem Provers", 16.10.2022, OvGU Magdeburg, First supervisor: Prof. Dr.-Ing. T. Mossakowski

Bachelor Theses (As Co-Supervisor)

• Egger, M. : "On Extending nanoCoP with the Arith Procedure", 04.02.2024, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz
• Repp, L. : "Extending the Automated Theorem Prover nanoCoP with Arithmetic Procedures",  09.09.2022, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz
• Münch, K. : "Entwicklung einer performanten und verlässlichen Schnittstelle für leanCoP-Ω", 04.04.2021, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz
• Behrens, A. : "Modernisierung von Legacy Beweissystemen", 30.09.2019, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz - PDF,BibTex
• Engelhard, C. : "Konzeption und Implementierung eines Interfaces zwischen SAT/SMT Solvern und automatischen Beweissystemen", 20.12.2018, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz
• Martin, J. : "Analyse und Prototypische Implementierung des SUP-INF-Algorithmus für Presburger Arithmetik", 26.05.2017, University of Potsdam, First supervisor: Prof. Dr. Chr. Kreitz

• Winter Term 2024/2025: Correct-by-Construction Software Engineering (Lecturer)
• Summer Term 2024: Software Engineering II (Assistant)
• Summer term 2020: Theoretical Computer Science II - Efficient Algorithms (Co-Lecturer)
• Summer term 2019: Theoretical Computer Science II - Efficient Algorithms (Co-Lecturer)
• Winter term 2017/2018: Theoretical Computer Science I - Modelling: Automatons and formal languages (Co-Lecturer)
• Winter term 2016/2017: Theoretical Computer Science I - Modelling: Automatons and formal languages (Co-Lecturer)
• Summer term 2015: ATP Construction Project (Lecturer, under supervision of Prof. Dr. Kreitz )
• Winter term 2014/2015: Seminar Theoretische Informatik - Methoden des automatischen Theorembeweisens (Lecturer, under supervision of Prof. Dr. Kreitz )
• Summer term 2014: Seminar Theoretische Informatik - Funktionale Programmierung mit Haskell (Co-Lecturer)