scientific article; zbMATH DE number 7649972
From MaRDI portal
Publication:5875432
Cites work
- 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
- scientific article; zbMATH DE number 2013597 (Why is no real title available?)
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- 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
(6)- Relation-algebraic verification of Borůvka's minimum spanning tree algorithm
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- A formal analysis of algorithms for matroids and greedoids
- Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
- Priority Search Trees
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
Describes a project that uses
Uses Software
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)
