I studied computer science, with mathematics as minor subject, at the TU München from 2009 until 2015. From October 2016 to February 2021 I was a Ph.D. student at the Chair for Logic and Verification.
:  orcid.org/000000034306869X 

My interests are mainly formalizing mathematics in higherorder logic and verifying software upon this. I'm also interested in processing of natural language proofs. My current work mostly is related to the Isabelle theorem prover and verified analysis of algorithms.
Publications
Dissertation

PhD thesis: Verified Quantitative Analysis of Imperative Algorithms
Maximilian P. L. Haslbeck
Fakultät für Informatik, Technische Universiät München. November 2021.
Journal Articles

For a Few Dollars More  Verified FineGrained Algorithm Analysis Down to LLVM
Maximilian P. L. Haslbeck, Peter Lammich
In TOPLAS. Preprint
Conference Proceedings

For a Few Dollars More  Verified FineGrained Algorithm Analysis Down to LLVM
Maximilian P. L. Haslbeck, Peter Lammich
In ESOP 2021. ESOP21 Talk (17min) 
Verified Textbook Algorithms. A Biased Survey
Tobias Nipkow, Manuel Eberl, Maximilian P. L. Haslbeck
In ATVA 2020 (Invited Paper). 
Refinement with Time  Refining the Runtime of Algorithms in Isabelle/HOL
Maximilian P. L. Haslbeck, Peter Lammich
In ITP 2019. 
Competitive Proving for Fun
Maximilian P. L. Haslbeck, Simon Wimmer
In LuxLogAI 2018 (Student / Workshop Papers) 
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Bohua Zhan, Maximilian P. L. Haslbeck
In IJCAR 2018. Repository 
Hoare Logics for Time Bounds
Maximilian P. L. Haslbeck, Tobias Nipkow
In TACAS 2018, LNCS, 2018. 
Verified Analysis of List Update Algorithms
Maximilian P. L. Haslbeck, Tobias Nipkow
In FSTTCS 2016, LNCS, 2016.
Archive of Formal Proofs

Kruskal's Algorithm for Minimum Spanning Forest
Maximilian P. L. Haslbeck, Peter Lammich, Julian Biendarra
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, https://www.isaafp.org/entries/Hoare_Time.html, February 2019, Formal proof development. 
Hoare Logics for Time Bounds
Maximilian P. L. Haslbeck, Tobias Nipkow
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, https://www.isaafp.org/entries/Hoare_Time.html, February 2018, Formal proof development. 
Analysis of List Update Algorithms
Maximilian P. L. Haslbeck, Tobias Nipkow
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, https://www.isaafp.org/entries/List_Update.shtml, February 2016, Formal proof development.
Master's Thesis

Verified Analysis of Algorithms for the List Update Problem
Institut für Informatik, TU München. September 2015.
Bachelor's Thesis

Verified decision procedures for the equivalence of regular expressions
Institut für Informatik, TU München. July 2013.
Projects
Supervised Students
 Bernhard Pöttinger  MA  Verification of the Flow Framework from "Local Reasoning for Global Graph Properties"
 Christopher Aßmus  BA  Testing with a Verified Oracle: Generating Inputs with Fuzzing
 Benjamin Rickels  BA  Testing with a Verified Oracle: Developing a Framework and Generating Test Cases via Symbolic Execution
 Simon Griebel  MA  Verification of the DecreaseKey Operation in Fibonacci Heaps in ImperativeHOL
 Fabian Hellauer  MA  Verification of an Approximation Algorithm for the Metric Travelling Salesperson Problem
 Adrián Löwenberg Casas  BA  Proof of the Amortized Time Complexity of an Efficient UnionFind Data Structure in Isabelle/HOL
 Daniel Stüwe  MA  Verification of Fibonacci Heaps in ImperativeHOL
Proving for Fun
At Proving for Fun we host proving contests and homework submission (in Isabelle). Feel free to solve the problems, spread the word and give feedback.
Collaborative Proving Projects

Complexity theory and polynomialtime reductions in Isabelle/HOL
This repository sets out to verify Karp's 21 Problems. Also we want to tackle formalizing Complexity Theory results in Isabelle/HOL, in particular the CookLevin theorem. Feel free to join!

Graph Theories in Isabelle/HOL
There are many ways of modelling graphs formally. It seems that there has not evolved one "best" approach, especially when it comes to undirected graphs. This repository collects several graph formalizations and comes with adapters between them. Feel free to join! 
Machine Learning verified
This repository collects efforts to formalize results on machine learning following the book Understanding Machine Learning by ShalevShwartz and BenDavid. Feel free to join!
Teaching
 Winter 20/21: organizer of the lab course Contributing to an OpenSource Project
 Summer 20: organizer of the Automated Reasoning seminar and the Specification and Verification lab course
 Winter 19/20: organizer of the Specification and Verification lab course
 Summer 19: organizer of the Specification and Verification lab course
 Summer 18: organizer of the Formal Proof in Mathematics and Computer Science Seminar
 Summer 17: coorganizer of the Formal Proof in Mathematics and Computer Science Seminar