A library of formally verified software for planning and model checking
Formally verified validator for planning problems and solutions specified in PDDL (supporting the STRIPS planning fragment) [github]
M. Abdulaziz and P. Lammich, ‘A Formally Verified Validator for Classical Planning Problems and Solutions’, in the 30th International Conference on Tools with Artificial Intelligence (ICTAI), 2018. doi: 10.1609/aaai.v36i9.21197.
M. Abdulaziz and L. Koller, ‘Formal semantics and formally verified validation for temporal planning.’, in the 36th AAAI Conference on Artificial Intelligence (AAAI), 2022. doi: 10.1609/aaai.v36i9.21197.
Formally verified validators for planning problems and solutions specified in Fast-Downward's translator format [Download]
A formally verified SAT-based planner for planning problems and solutions specified in Fast-Downward's translator format [github]
M. Abdulaziz and F. Kurz, ‘Formally verified SAT-Based AI planning’, in the 37th AAAI Conference on Artificial Intelligence (AAAI), 2023. doi: 10.1609/aaai.v37i12.26714.
Formally verfied implementations of (Gauss-Seidel) value iteration and (modified) policy iteration for tabular (explicit) MDPs [github]
M. Schäffeler and M. Abdulaziz, ‘Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes’, in the 37th AAAI Conference on Artificial Intelligence (AAAI), 2023. doi: 10.1609/aaai.v37i12.26759.
A formally verfied implementation of Guestrin's seminal approximate policy iteration algorithm for solving factored MDPs [github]
M. Schäffeler and M. Abdulaziz, ‘Formally Verified Approximate Policy Iteration’. in the 39th AAAI Conference on Artificial Intelligence (AAAI), 2025. doi: 10.48550/arXiv.2406.07340.
Mohammad Abdulaziz, Maximilian Schäffeler, Lukas Koller, Friedrich Kurz, Peter Lammich