3 citations · 10 across the 13 of their papers we have counts for
16 papers
Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens +3
Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annot…
Formal Primal-Dual Algorithm Analysis
Mohammad Abdulaziz, Thomas Ammer, Christoph Madlener
We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example…
A Formal Analysis of Capacity Scaling Algorithms for Minimum-Cost Flows
Mohammad Abdulaziz, Thomas Ammer
We present formalisations of the correctness of executable algorithms to solve minimum-cost flow problems in Isabelle/HOL. Two of the algorithms are based on the technique of scali…
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…
A Formal Correctness Proof of Edmonds' Blossom Shrinking Algorithm
Mohammad Abdulaziz, Kurt Mehlhorn
We present the first formal correctness proof of Edmonds' blossom shrinking algorithm for maximum cardinality matching in general graphs. We focus on formalising the mathematical s…
Formally Verified Approximate Policy Iteration
Maximilian Schäffeler, Mohammad Abdulaziz
We formally verify an algorithm for approximate policy iteration on Factored Markov Decision Processes using the interactive theorem prover Isabelle/HOL. Next, we show how the form…
A Formal Analysis of RANKING
Mohammad Abdulaziz, Christoph Madlener
We describe a formal correctness proof of RANKING, an online algorithm for online bipartite matching. An outcome of our formalisation is that it shows that there is a gap in all co…
Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes
Maximilian Schäfeller, Mohammad Abdulaziz
We formally verify executable algorithms for solving Markov decision processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on existing formalizations of probabi…
Formal Semantics and Formally Verified Validation for Temporal Planning
Mohammad Abdulaziz, Lukas Koller
We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive f…
Cost Optimal Planning as Satisfiability
Mohammad Abdulaziz
We investigate upper bounds on the length of cost optimal plans that are valid for problems with 0-cost actions. We employ these upper bounds as horizons for a SAT-based encoding o…
Formally Verified SAT-Based AI Planning
Mohammad Abdulaziz, Friedrich Kurz
We present an executable formally verified SAT encoding of classical AI planning. We use the theorem prover Isabelle/HOL to perform the verification. We experimentally test the ver…
Computing Plan-Length Bounds Using Lengths of Longest Paths
Mohammad Abdulaziz, Dominik Berger
We devise a method to exactly compute the length of the longest simple path in factored state spaces, like state spaces encountered in classical planning. Although the complexity o…
Trustworthy Graph Algorithms
Mohammad Abdulaziz, Kurt Mehlhorn, Tobias Nipkow
The goal of the LEDA project was to build an easy-to-use and extendable library of correct and efficient data structures, graph algorithms and geometric algorithms. We report on th…