scientific article; zbMATH DE number 7649972

DOI10.4230/LIPICS.ITP.2019.23MaRDI QIDQ5875432FDOQ5875432

Authors: Peter Lammich, Tobias Nipkow 

Publication date: 3 February 2023

Title of this publication is not available (Why is that?)

zbMATH Keywords

verificationPrim's algorithmIsabelleDijkstra's algorithmpriority queue

Mathematics Subject Classification ID

Cites Work

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

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

Uses Software

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

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)