Trustworthy Graph Algorithms (Invited Talk)

DOI10.4230/LIPICS.MFCS.2019.1MaRDI QIDQ5092359zbMATH OpenOpenAlexFDO

Authors Mohammad Abdulaziz, K. Mehlhorn, Tobias Nipkow

Publication date 21 July 2022

Full work available at URL https://arxiv.org/abs/1907.04065

zbMATH Keywords

graph algorithmsIsabellecertifying algorithmsLEDAformal correct proofs

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• A framework for the verification of certifying computations
• A theory of alternating paths and blossoms for proving correctness of the \(O(\sqrt{V}E)\) general graph maximum matching algorithm
• LEDA. A platform for combinatorial and geometric computing. 2-part set
• Verified efficient implementation of Gabow's strongly connected component algorithm
• Verified approximation algorithms

Cites work

• scientific article; zbMATH DE number 1368469 (Why is no real title available?)
• A formally verified compiler back-end
• A graph library for Isabelle
• A verified compiler from Isabelle/HOL to CakeML
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Algorithms – ESA 2004
• An Efficient Implementation of Edmonds' Algorithm for Maximum Matching on Graphs
• Automatic Data Refinement
• Bridging the Gap: Automatic Verified Abstraction of C
• CakeML
• Certifying algorithms
• Characteristic formulae for the verification of imperative programs
• Code generation via higher-order rewrite systems
• Combinatorial optimization. Theory and algorithms.
• Data refinement in Isabelle/HOL
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Formally verified algorithms for upper-bounding state space diameters
• Imperative Functional Programming with Isabelle/HOL
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Maximum matching and a polyhedron with 0,1-vertices
• Maximum network flow with floating point arithmetic.
• Proof-producing translation of higher-order logic into pure and stateful ML
• Refinement to imperative HOL
• Towards exact geometric computation

Cited in

(4)

• A formal correctness proof of Edmonds' blossom shrinking algorithm
• A formal analysis of capacity scaling algorithms for minimum cost flows
• Discovering and certifying lower bounds for the online bin stretching problem
• Incorporating a database of graphs into a proof assistant

This page was built for publication: Trustworthy Graph Algorithms (Invited Talk)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5092359)