scientific article; zbMATH DE number 7649972

DOI10.4230/LIPIcs.ITP.2019.23MaRDI QIDQ5875432

Peter Lammich, Tobias Nipkow

Publication date: 3 February 2023

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

verificationpriority queueDijkstra's algorithmPrim's algorithmIsabelle

Mathematics Subject Classification ID

Related Items (2)

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on two problems in connexion with graphs
• Isabelle/HOL. A proof assistant for higher-order logic
• A graph library for Isabelle
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Concrete Semantics
• Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm
• Finger trees: a simple general-purpose data structure
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Code Generation via Higher-Order Rewrite Systems
• Priority Search Trees
• Purely Functional Data Structures
• Program-ing finger trees in C <scp>oq</scp>
• Characteristic formulae for the verification of imperative programs
• A simple implementation technique for priority search queues
• Why3 — Where Programs Meet Provers

This page was built for publication: