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

DOI10.1007/978-3-030-81688-9_37zbMath1493.68216OpenAlexW3185067705MaRDI QIDQ832310

Anshuman Mohan, Wei Xiang Leow, Aquinas Hobor

Publication date: 25 March 2022

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)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on two problems in connexion with graphs
• On the shortest spanning subtree of a graph and the traveling salesman problem
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Verifying minimum spanning tree algorithms with Stone relation algebras
• A graph library for Isabelle
• Simpler proofs with decentralized invariants
• Automated Verification of Practical Garbage Collectors
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Formalizing the Edmonds-Karp Algorithm
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• The ramifications of sharing in data structures
• Dafny: An Automatic Program Verifier for Functional Correctness
• Verifying Concurrent Graph Algorithms
• Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm
• A Unified Approach to Path Problems
• Regular Algebra Applied to Path-finding Problems
• Local Reasoning for Global Graph Properties
• Efficient Verified Implementation of Introsort and Pdqsort
• Characteristic formulae for the verification of imperative programs
• Fun with semirings
• Formal certification of a compiler back-end or
• Interactive proofs in higher-order concurrent separation logic
• Theorem Proving in Higher Order Logics
• Program Logics for Certified Compilers
• Correct Hardware Design and Verification Methods