3 citations · 10 across the 13 of their papers we have counts for
4 papers · 1 filter
Formally Verified Certification of Unsolvability of Temporal Planning Problems
David Wang, Mohammad Abdulaziz
We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using…
A Formal Analysis of Algorithms for Matroids and Greedoids
Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram +1
We present a formal analysis, in Isabelle/HOL, of optimisation algorithms for matroids, which are useful generalisations of combinatorial structures that occur in optimisation, and…
Proof-Producing Translation of Functional Programs into a Time \& Space Reasonable Model
Kevin Kappelmann, Fabian Huch, Lukas Stevens +1
We present a semi-automated framework to construct and reason about programs in a deeply-embedded while-language. The while-language we consider is a simple computation model that…
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz +2
We present an efficiently executable, formally verified implementation of interval iteration for MDPs. Our correctness proofs span the entire development from the high-level abstra…