Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms

DOI10.1007/978-3-030-81688-9_37MaRDI QIDQ832310zbMATH OpenOpenAlexFDO

Authors Anshuman Mohan, Wei Xiang Leow, Aquinas Hobor

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-81688-9_37

zbMATH Keywords

graph algorithmsseparation logicCoqVST

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Relation-algebraic verification of Prim's minimum spanning tree algorithm
• An algebraic framework for minimum spanning tree problems
• scientific article; zbMATH DE number 177565
• scientific article; zbMATH DE number 1264417
• scientific article; zbMATH DE number 2013597

Cites work

• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 5937963 (Why is no real title available?)
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• scientific article; zbMATH DE number 7649972 (Why is no real title available?)
• A Unified Approach to Path Problems
• A graph library for Isabelle
• A note on two problems in connexion with graphs
• Automated verification of practical garbage collectors
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Characteristic formulae for the verification of imperative programs
• Dafny: an automatic program verifier for functional correctness
• Efficient Verified Implementation of Introsort and Pdqsort
• Executing the formal semantics of the Accellera property specification language by mechanised theorem proving
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Formalizing the Edmonds-Karp algorithm
• Fun with semirings
• Interactive proofs in higher-order concurrent separation logic
• Introduction to algorithms.
• Local reasoning for global graph properties
• On the shortest spanning subtree of a graph and the traveling salesman problem
• Program logics for certified compilers
• Regular Algebra Applied to Path-finding Problems
• Relation-algebraic verification of Prim's minimum spanning tree algorithm
• Simpler proofs with decentralized invariants
• The algorithm design manual
• The ramifications of sharing in data structures
• Theorem Proving in Higher Order Logics
• Verified efficient implementation of Gabow's strongly connected component algorithm
• Verifying concurrent graph algorithms
• Verifying minimum spanning tree algorithms with Stone relation algebras
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Viper: a verification infrastructure for permission-based reasoning

Cited in

(1)

• Relation-algebraic verification of Prim's minimum spanning tree algorithm

Describes a project that uses

Uses Software

• Coq
• Dafny
• BLAST
• z3
• Stony Brook
• Boogie
• Toolchain
• HIP
• Smallfoot
• VerCors
• Viper
• VACID-0
• Edmonds-Karp
• Graph Theory
• Stone Algebras
• Gabow SCC

This page was built for publication: Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms

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