scientific article; zbMATH DE number 7649969

DOI10.4230/LIPICS.ITP.2019.20MaRDI QIDQ5875428zbMATH OpenFDO

Authors Peter Lammich, Maximilian P. L. Haslbeck

Publication date 3 February 2023

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2019.20

zbMATH Keywords

algorithmsIsabelleprogram verificationrefinementrun timeseparation logictime complexity analysis

Mathematics Subject Classification ID

Cites work

• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Amortised resource analysis with separation logic
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Characteristic formulae for the verification of imperative programs
• Formalizing the Edmonds-Karp algorithm
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Refinement to Imperative/HOL
• Verified efficient implementation of Gabow's strongly connected component algorithm
• Verified model checking of timed automata
• Verifying asymptotic time complexity of imperative programs in Isabelle
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

Cited in

(4)

• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• Efficient Verified Implementation of Introsort and Pdqsort
• Simplified and verified: a second look at a proof-producing union-find algorithm
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms

Describes a project that uses

Uses Software

• Edmonds-Karp
• Archive of 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 Q5875428)