Maximilian Schäffeler

2 accepted papers

2025

Formally Verified Approximate Policy Iteration

Maximilian Schäffeler, Mohammad Abdulaziz

AAAI 2025technical

We present a methodology based on interactive theorem proving that facilitates the development of verified implementations of algorithms for solving factored Markov Decision Processes. As a case study, we formally verify an algorithm for approximate policy iteration in the proof assistant Isabelle/H…

Cited by 1 Source ↗PDF ↗code ↗Scholar ↗

2023

Formally Verified Solution Methods for Markov Decision Processes

Maximilian Schäffeler, Mohammad Abdulaziz

AAAI 2023technical

We formally verify executable algorithms for solving Markov decision processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on existing formalizations of probability theory to analyze the expected total reward criterion on finite and infinite-horizon problems. Our developments for…

Cited by 9 Source ↗PDF ↗code ↗Scholar ↗