Verified Algorithms for Solving Markov Decision Processes. - Maximilian Schäffeler; Mohammad Abdulaziz (Arch. Formal Proofs, 2021)

Markov Decision Processes with Rewards. - Maximilian Schäffeler; Mohammad Abdulaziz (Arch. Formal Proofs, 2021)

Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes. - Maximilian Schäffeler; Mohammad Abdulaziz (CoRR, 2022)

Formally Verified Solution Methods for Markov Decision Processes. - Maximilian Schäffeler; Mohammad Abdulaziz (AAAI, 2023)

Formally Verified Approximate Policy Iteration. - Maximilian Schäffeler; Mohammad Abdulaziz (AAAI, 2025)

A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs. - Bram Kohlen; Maximilian Schäffeler; Mohammad Abdulaziz; Arnd Hartmanns; Peter Lammich (CAV (2), 2025)

Fixed Point Certificates for Reachability and Expected Rewards in MDPs. - Krishnendu Chatterjee; Tim Quatmann; Maximilian Schäffeler; Maximilian Weininger; Tobias Winkler 001; Daniel Zilken (TACAS (2), 2025)

Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs. - Krishnendu Chatterjee; Tim Quatmann; Maximilian Schäffeler; Maximilian Weininger; Tobias Winkler 001; Daniel Zillken (Zenodo, 2025)