scientific article; zbMATH DE number 7649972

DOI10.4230/LIPICS.ITP.2019.23MaRDI QIDQ5875432zbMATH OpenFDO

Authors Peter Lammich, Tobias Nipkow

Publication date 3 February 2023

zbMATH Keywords

verificationPrim's algorithmIsabelleDijkstra's algorithmpriority queue

Mathematics Subject Classification ID

Cites work

• scientific article; zbMATH DE number 2013597 (Why is no real title available?)
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• A graph library for Isabelle
• A note on two problems in connexion with graphs
• A simple implementation technique for priority search queues
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Characteristic formulae for the verification of imperative programs
• Code generation via higher-order rewrite systems
• Concrete semantics. With Isabelle/HOL
• Finger trees: a simple general-purpose data structure
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Introduction to algorithms.
• Isabelle/HOL. A proof assistant for higher-order logic
• Priority Search Trees
• Program-ing finger trees in Coq
• Purely Functional Data Structures
• Relation-algebraic verification of Prim's minimum spanning tree algorithm
• Why3 -- where programs meet provers

Cited in

(3)

• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• Relation-algebraic verification of Borůvka's minimum spanning tree algorithm
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction

Describes a project that uses

Uses Software

• Archive Formal Proofs
• Dijkstra Shortest Path
• WhyML
• Boogie
• Why3
• Isabelle/HOL
• HOL-Boogie

This page was built for publication:

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