Maximilian Schäffeler

About me

I am currently (since August 2021) a doctoral candidate in Computer Science at the Chair for Logic and Verification supervised by Prof. Nipkow and Dr. Mohammad Abdulaziz. I am interested in the formalization of solution methods for Markov decision processes (MDPs) in the interactive theorem prover Isabelle.

Beginning in 2015, I did my Bachelors and Masters in Computer Science at the Technical University of Munich. During my studies I specialized in IT security, functional programming and formal methods. For my Master’s thesis Verified Solution Methods for Markov Decision Processes I verified the value iteration and policy iteration algorithms in Isabelle/HOL.

If you are interested in collaborating on a project, feel free to contact me!

Publications

• A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs (2025)
  by Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich
  Available on arXiv
• Fixed Point Certificates for Reachability and Expected Rewards in MDPs (2025)
  by Krishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Zilken
  To be published in TACAS 2025
  Preprint available on arXiv
• Formally Verified Approximate Policy Iteration (2025)
  by Maximilian Schäffeler, Mohammad Abdulaziz
  To be published in: Proceedings of the 39th AAAI Conference on Artificial Intelligence
  Preprint available on arXiv
• Formally Verified Solution Methods for Markov Decision Processes (2023)
  by Maximilian Schäffeler, Mohammad Abdulaziz
  Published in: Proceedings of the 37th AAAI Conference on Artificial Intelligence, DOI: 10.1609/aaai.v37i12.26759

Entries in the Archive of Formal Proofs (AFP)

• Markov Decision Processes with Rewards (2021)
  by Maximilian Schäffeler, Mohammad Abdulaziz
• Verified Algorithms for Solving Markov Decision Processes (2021)
  by Maximilian Schäffeler, Mohammad Abdulaziz

Contact