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/0000-0003-4306-869X |
|---|
My interests are mainly formalizing mathematics in higher-order 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 Fine-Grained Algorithm Analysis Down to LLVM
Maximilian P. L. Haslbeck, Peter Lammich
In TOPLAS. Preprint
Conference Proceedings
-
For a Few Dollars More - Verified Fine-Grained 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 Run-time 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.isa-afp.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.isa-afp.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.isa-afp.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 Decrease-Key Operation in Fibonacci Heaps in Imperative-HOL
- 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 Union-Find Data Structure in Isabelle/HOL
- Daniel Stüwe - MA - Verification of Fibonacci Heaps in Imperative-HOL
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 polynomial-time 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 Cook-Levin 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 Shalev-Shwartz and Ben-David. Feel free to join!
Teaching
-
Winter 20/21: organizer of the lab course Contributing to an Open-Source 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: co-organizer of the Formal Proof in Mathematics and Computer Science Seminar
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 Cook-Levin theorem. Feel free to join!
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!
This repository collects efforts to formalize results on machine learning following the book Understanding Machine Learning by Shalev-Shwartz and Ben-David. Feel free to join!