Trustworthy Graph Algorithms (Invited Talk)
From MaRDI portal
Publication:5092359
DOI10.4230/LIPIcs.MFCS.2019.1OpenAlexW2991894924MaRDI QIDQ5092359
Tobias Nipkow, Mohammad Abdulaziz, Kurt Mehlhorn
Publication date: 21 July 2022
Full work available at URL: https://arxiv.org/abs/1907.04065
Related Items
Cites Work
- Unnamed Item
- Certifying algorithms
- Towards exact geometric computation
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- Formally verified algorithms for upper-bounding state space diameters
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Refinement to imperative HOL
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
- A graph library for Isabelle
- A verified compiler from Isabelle/HOL to CakeML
- Maximum network flow with floating point arithmetic.
- A formally verified compiler back-end
- Proof-producing translation of higher-order logic into pure and stateful ML
- Bridging the Gap: Automatic Verified Abstraction of C
- Imperative Functional Programming with Isabelle/HOL
- Code Generation via Higher-Order Rewrite Systems
- An Efficient Implementation of Edmonds' Algorithm for Maximum Matching on Graphs
- Characteristic formulae for the verification of imperative programs
- Automatic Data Refinement
- Data Refinement in Isabelle/HOL
- CakeML
- Algorithms – ESA 2004
- Maximum matching and a polyhedron with 0,1-vertices
- Logic for Programming, Artificial Intelligence, and Reasoning
- Combinatorial optimization. Theory and algorithms.
