Mario Frank studierte von 2007 bis 2013 Informatik an der Universität Potsdam und schloss dieses mit einem Diplom ab. Im Zuge seines Studiums beschäftigte er sich ausgiebig mit der Verarbeitung von Korpora und arbeitete dabei für und mit der Korpuslinguistik der HU Berlin, der Computerlinguistik der Universität Potsdam und der Ruhr-Universität Bochum zusammen. Zum Ende seines Studiums spezialisierte er sich auf die automatisierte Verarbeitung - im Speziellen Reduktion - von logischen Formelmengen unter Anwendung von Konzepten der Computerlinguistik. In diesem Zuge nahm er in Kooperation mit Dr. Jens Otten zwei mal an der CADE ATP Systems Competition teil.

Nach Beendigung seines Studiums begann er sein Promotionsvorhaben am Lehrstuhl Theoretische Informatik unter der Betreuung von Prof. Dr. Christoph Kreitz im Themengebiet der interaktiven und automatischen Deduktion. 2014/2015 nahm er am Junior Teaching Professionals Programm der PoGS teil und sammelte in diesem Zuge seine erste Erfahrung in der begleitenden und eigenverantwortlichen Hochschullehre.

Von 2014 bis 2016 war er technischer Mitarbeiter in den Projekten "Reisen.UP" und "Beschaffung.UP" der Abteilung CIO. Dabei unterstützte er die Projekte mit theoretischen Kenntnissen in der Komplexitätstheorie und Logik sowie praktisch in der Software-Entwicklung, Modellierung, Konzeption und Anforderungsanalyse. Im Zeitraum 2016 bis zum 30.06.2021 war er wissenschaftlicher Mitarbeiter am Lehrstuhl Theoretische Informatik. Seit 01.07.2021 arbeitet er am Lehrstuhl Theoretische Informatik im Verbundprojekt VERSECLOUD.

• Interaktives und Automatisches Theorembeweisen
• Frameworks zur Synthetisierung von Software
• Beweisvisualisierung
• Usability von interaktiven Theorembeweisern

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

Masterarbeiten (Zweitbetreuer/-Gutachter)

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

Bachelorarbeiten (Zweitbetreuer/-Gutachter)

• Repp, L. : "Extending the Automated Theorem Prover nanoCoP with Arithmetic Procedures",  09.09.2022, Universität Potsdam, Erstbetreuer: Prof. Dr. Chr. Kreitz
• Münch, K. : "Entwicklung einer performanten und verlässlichen Schnittstelle für leanCoP-Ω", 04.04.2021, Universität Potsdam, Erstbetreuer: Prof. Dr. Chr. Kreitz
• Behrens, A. : "Modernisierung von Legacy Beweissystemen", 30.09.2019, Universität Potsdam, Erstbetreuer: 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, Erstbetreuer: Prof. Dr. Chr. Kreitz
• Martin, J. : "Analyse und Prototypische Implementierung des SUP-INF-Algorithmus für Presburger Arithmetik", 26.05.2017, Universität Potsdam, Erstbetreuer: Prof. Dr. Chr. Kreitz

• Sommersemester 2020: Theoretische Informatik II - Effiziente Algorithmen (Assistent: Übungsleitung, Übungs-, Testat- und Klausurkonzeption)
• Sommersemester 2019: Theoretische Informatik II - Effiziente Algorithmen (Assistent: Übungsleitung, Übungs-, Testat- und Klausurkonzeption)
• Wintersemester 2017/2018: Theoretische Informatik I - Modellierungskonzepte - Automaten und formale Sprachen (Assistent: Übungsleitung, Übungs-, Testat- und Klausurkonzeption)
• Wintersemester 2016/2017: Theoretische Informatik I - Modellierungskonzepte - Automaten und formale Sprachen (Assistent: Übungsleitung, Übungs-, Testat- und Klausurkonzeption)
• Sommersemester 2015: ATP Construction Project (Dozent, unter Betreuung durch Prof. Dr. C. Kreitz )
• Wintersemester 2014/2015: Seminar Theoretische Informatik - Methoden des automatischen Theorembeweisens (Dozent, unter Betreuung durch Prof. Dr. C. Kreitz )
• Sommersemester 2014: Seminar Theoretische Informatik - Funktionale Programmierung mit Haskell (Assistent: Übungskonzeption)

Als SHK/WHK:

• Tutor für Theoretische Informatik I (Wintersemester 2012/2013) und Theoretische Informatik II (Sommersemester 2012)
• Tutor für Verteilte Systeme (Sommersemester 2012)
• Tutor für Programmierung - Programming (Sommersemester 2011)
• Tutor für Rechner- und Netzbetrieb (Wintersemester 2010/2011 sowie 2011/2012)

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. Diplomarbeit, veröffentlicht 2014 auf dem Publikationsserver der Universität Potsdam

Frank, M (2012/2014). ARDE - Technical Report. Studentische Arbeit, veröffentlicht 2014 auf dem Publikationsserver der Universität 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 sind unter meinem ORCID-Profil zu finden

Artifact Evaluation Committee

• 18th International Conference on integrated Formal Methods (iFM 2023)

Wettbewerbe

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