Exploiting satisfiability modulo theories for analog layout automation. - Sherif M. Saif; Mohamed Dessouky; Salwa M. Nassar; Hazem M. Abbas; M. Watheq El-Kharashi; Mohammad Abdulaziz (IDT, 2014)

Exploiting Symmetries by Planning for a Descriptive Quotient. - Mohammad Abdulaziz; Michael Norrish; Charles Gretton (IJCAI, 2015)

Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems. - Mohammad Abdulaziz; Charles Gretton; Michael Norrish (ITP, 2015)

A State-Space Acyclicity Property for Exponentially Tighter Plan Length Bounds. - Mohammad Abdulaziz; Charles Gretton; Michael Norrish (ICAPS, 2017)

A Formally Verified Validator for Classical Planning Problems and Solutions. - Mohammad Abdulaziz; Peter Lammich (ICTAI, 2018)

An Isabelle/HOL formalisation of Green's Theorem. - Mohammad Abdulaziz; Lawrence C. Paulson (Arch. Formal Proofs, 2018)

Upper Bounding Diameters of State Spaces of Factored Transition Systems. - Friedrich Kurz; Mohammad Abdulaziz (Arch. Formal Proofs, 2018)

Formally Verified Algorithms for Upper-Bounding State Space Diameters. - Mohammad Abdulaziz; Michael Norrish; Charles Gretton (J. Autom. Reason., 2018)

Plan-Length Bounds: Beyond 1-Way Dependency. - Mohammad Abdulaziz (AAAI, 2019)

A Verified Compositional Algorithm for AI Planning. - Mohammad Abdulaziz; Charles Gretton; Michael Norrish (ITP, 2019)

Trustworthy Graph Algorithms (Invited Talk). - Mohammad Abdulaziz; Kurt Mehlhorn; Tobias Nipkow (MFCS, 2019)

Trustworthy Graph Algorithms. - Mohammad Abdulaziz; Kurt Mehlhorn; Tobias Nipkow (CoRR, 2019)

Verified SAT-Based AI Planning. - Mohammad Abdulaziz; Friedrich Kurz (Arch. Formal Proofs, 2020)

AI Planning Languages Semantics. - Mohammad Abdulaziz; Peter Lammich (Arch. Formal Proofs, 2020)

Computing Plan-Length Bounds Using Lengths of Longest Paths. - Mohammad Abdulaziz; Dominik Berger (AAAI, 2021)

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)

Cost Optimal Planning as Satisfiability. - Mohammad Abdulaziz (CoRR, 2021)

Formal Semantics and Formally Verified Validation for Temporal Planning. - Mohammad Abdulaziz; Lukas Koller (AAAI, 2022)

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

Formally Verified SAT-Based AI Planning. - Mohammad Abdulaziz; Friedrich Kurz (AAAI, 2023)

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

A Formal Analysis of RANKING. - Mohammad Abdulaziz; Christoph Madlener (ITP, 2023)

Interactive Theorem Provers: Applications in AI, Opportunities, and Challenges. - Mohammad Abdulaziz (AAAI, 2024)

A Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows. - Mohammad Abdulaziz; Thomas Ammer (ITP, 2024)

A Formal Correctness Proof of Edmonds' Blossom Shrinking Algorithm. - Mohammad Abdulaziz (CoRR, 2024)

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)

Elementary Graph Traversal Algorithms. - Mohammad Abdulaziz (Arch. Formal Proofs, 2025)

Proof-Producing Translation of Functional Programs into a Time & Space Reasonable Model. - Kevin Kappelmann; Fabian Huch; Lukas Stevens; Mohammad Abdulaziz (CoRR, 2025)

A Formal Analysis of Algorithms for Matroids and Greedoids. - Mohammad Abdulaziz; Thomas Ammer; Shriya Meenakshisundaram; Adem Rimpapa (CoRR, 2025)