Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
DOI10.1007/978-3-030-81688-9_37zbMATH Open1493.68216OpenAlexW3185067705MaRDI QIDQ832310FDOQ832310
Authors: 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
Recommendations
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)
Cites Work
- Dafny: an automatic program verifier for functional correctness
- The algorithm design manual
- Formalizing the Edmonds-Karp algorithm
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- On the shortest spanning subtree of a graph and the traveling salesman problem
- A note on two problems in connexion with graphs
- Introduction to algorithms.
- Characteristic formulae for the verification of imperative programs
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Title not available (Why is that?)
- Regular Algebra Applied to Path-finding Problems
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Theorem Proving in Higher Order Logics
- Executing the formal semantics of the Accellera property specification language by mechanised theorem proving
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- A Unified Approach to Path Problems
- 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
- The ramifications of sharing in data structures
- Verifying concurrent graph algorithms
- Relation-algebraic verification of Prim's minimum spanning tree algorithm
- Local reasoning for global graph properties
- Efficient Verified Implementation of Introsort and Pdqsort
- Title not available (Why is that?)
- Fun with semirings
- Interactive proofs in higher-order concurrent separation logic
- Program logics for certified compilers
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (1)
Uses Software
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)
