8 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…
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 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 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…