Zum Hauptinhalt springen

Dr. rer. nat Mario Frank

Wissenschaftlicher Mitarbeiter

Studienfachberatung I/CS, BAFöG-Beauftragter für Informatik, wissenschaftliche Koordination des Joint Lab

Campus Golm
Universität Potsdam
Institut für Informatik und Computational Science
Haus 70, Raum 2.46
An der Bahn 2
14476 Potsdam

Forschungsinteressen

  • Softwaresynthese and -Verifikation
  • Interaktives und automatisches Theorembeweisen
  • Beweisvisualisierung
  • Usability von Interaktiven Beweissystemen

Curriculum Vitae

Ausbildung

  • 2024 - Promotion zum "Dr. rer. nat" mit dem Thema "On Synthesising Linux Kernel Module Components from Coq Formalisations"
  • 2015 - Abschluss des "Junior Teaching Professionals" Programmes der Potsdam Graduate School
  • 2013 - Abschluss als "Dipl.-Inform"  mit dem Thema "TEMPLAR - Efficient Determination of Relevant Axioms in Big Formula Sets for Theorem Proving"

Wissenschaftliche und Technische Positionen

  • Seit 02/2026 - Wissenschaftlicher Mitarbeiter, Lehr- und Studienkoordination, Institut für Informatik
  • 07/2024-01/2026 - Wissenschaftlicher Mitarbeiter (PostDoc),  Lehrstuhl Software Engineering
  • 04/2024-07/2024 - Wissenschaftlicher Mitarbeiter,  Lehrstuhl Software Engineering
  • 07/2021-03/2024 - Wissenschaftlicher Mitarbeiter, Lehrstuhl Theoretische Informatik (Konsortialprojekt VERSECLOUD)
  • 2016-2021 - Wissenschaftlicher Mitarbeiter, Lehrstuhl Theoretische Informatik
  • 2014-2016 - Technischer Mitarbeiter in den Projekten "Reisen.UP" und "Beschaffung.UP" der CIO, Universität Potsdam

Publikationen

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.

Weitere Publikationen finden sich auf meinem ORCID Profil.

Fachvorträge

Frank, M. (2025): On Embedding Code Extracted From Coq Formalisations into Data Analysis Workflows. 5th conference for Research Software Engineering in Germany, 25-27.02.2025, KIT, Karlsruhe, Germany.

Frank, M.; Egger, M.; Otto, A.; Kreitz, Chr. (2023): Bringing Synthesised Software to a Real-World Microkernel Operating System. The 35th Symposium on Implementation and Application of Functional Languages, IFL 2023, 29-31.08.2023, Braga, Portugal.

Frinker, N.; Frank, M. (2023): Eine vertrauenswürdige, sichere Public Cloud - Utopie oder Realität?19. Deutscher IT-Sicherheitskongress, 10. - 11.05.2023.

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

Frank, M.; Kreitz, Chr. (2017): A theorem prover for scientific and educational purposes. ThEdu'17 - Theorem proving components for Educational software, 6 August 2017, Gothenburg, Sweden, at CADE26

Professionelle Aktivitäten

Journal Reviews

Sind auf meinem ORCID Profil hinterlegt.

Artifact Evaluation

Wettbewerbe

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

Mentorings

  • "Technovation Girls Germany: starke Apps von starken Mädchen" 2022/23
  • Google Summer of Code 2017, digiKam

Betreute Abschlussarbeiten

Masterarbeiten (Zweitbetreuer/Zweitgutachter)

  • 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, Hauptbetreuer: Prof. Dr.-Ing. T. Mossakowski

Bachelorarbeiten (Hauptbetreuer/Erstgutachter)

  • Hartmann, J.: "Untersuchung der Anwendbarkeit von AI-Tools zur Erstellung von 2D Texturen und Animationen im Game Development", 06.08.2025, Universität Potsdam, Zweitbetreuerin: Prof. Dr. A-L. Lamprecht
  • Schreitter Ritter von Schwarzenfeld, D.: "Extension with smaller tactics and an investigation of the feasibility of the ring tactic in Rocq's tactical language Ltac2", 26.04.2025, Universität Potsdam, Zweitbetreuerin: Prof. Dr. A-L. Lamprecht

Bachelorarbeiten (Zweitbetreuer/Zweitgutachter)

  • Langner, J.: "RSE und Sicherheit - Eine empirische Studie über die Verwendung von Sicherheitsaspekten in Research Software Engineering", 03.07.2025, Universität Potsdam, Hauptbetreuerin: Prof. Dr. A-L. Lamprecht
  • Henschel, M.: "Analyse von Workflow-Repositories zur Gewinnung von Erkenntnissen über die frühen Phasen des Workflow-Designs", 11.06.2025, Universität Potsdam, Hauptbetreuerin: Prof. Dr. A-L. Lamprecht
  • Hermann, P.: "Robotic Process Automation", 17.02.2025, Universität Potsdam, Hauptbetreuerin: Prof. Dr. A-L. Lamprecht
  • Yilmazcelik, A.: "Digitale Signaturen für den Prüfungsanmeldungsprozess: Integration und Bewertung verschiedener API-Dienste", 03.02.2025, Universität Potsdam, Hauptbetreuerin: Prof. Dr. A-L. Lamprecht
  • Egger, M. : "On Extending nanoCoP with the Arith Procedure", 04.02.2024, Universität Potsdam, Hauptbetreuer: Prof. Dr. Chr. Kreitz
  • Repp, L. : "Extending the Automated Theorem Prover nanoCoP with Arithmetic Procedures",  09.09.2022, Universität Potsdam, Hauptbetreuer: Prof. Dr. Chr. Kreitz
  • Münch, K. : "Entwicklung einer performanten und verlässlichen Schnittstelle für leanCoP-Ω", 04.04.2021, Universität Potsdam, Hauptbetreuer: Prof. Dr. Chr. Kreitz
  • Behrens, A. : "Modernisierung von Legacy Beweissystemen", 30.09.2019, Universität Potsdam, Hauptbetreuer: Prof. Dr. Chr. Kreitz - PDF,BibTex
  • Engelhard, C. : "Konzeption und Implementierung eines Interfaces zwischen SAT/SMT Solvern und automatischen Beweissystemen", 20.12.2018, Universität Potsdam, Hauptbetreuer: Prof. Dr. Chr. Kreitz
  • Martin, J. : "Analyse und Prototypische Implementierung des SUP-INF-Algorithmus für Presburger Arithmetik", 26.05.2017, Universität Potsdam,  Hauptbetreuer: Prof. Dr. Chr. Kreitz

Lehre

  • Wintersemester 2024/2025 und 2025/2026: Correct-by-Construction Software Engineering (Lehrender)
  • Sommersemester 2025: Software Engineering II (Übungsleitung)
  • Sommersemester 2024: Software Engineering II (Assistent)
  • Sommersemester 2019 und 2020: Theoretische Informatik II - Effiziente Algorithmen (Übungsleitung)
  • Wintersemester 2016/2017 und 2017/2018: Theoretische Informatik I - Modellierung: Automaten und formale Sprachen (Übungsleitung)
  • Sommersemester 2015: ATP Construction Project (Lehrender, betreut durch Prof. Dr. Kreitz )
  • Wintersemester 2014/2015: Seminar Theoretische Informatik - Methoden des automatischen Theorembeweisens (Lehrender, betreut durch Prof. Dr. Kreitz )
  • Sommersemester 2014: Seminar Theoretische Informatik - Funktionale Programmierung mit Haskell (Übungsleitung)