scientific article; zbMATH DE number 7649969

DOI10.4230/LIPIcs.ITP.2019.20MaRDI QIDQ5875428

Peter Lammich, Maximilian P. L. Haslbeck

Publication date: 3 February 2023

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

zbMATH Keywords

algorithmsrefinementseparation logicprogram verificationIsabelletime complexity analysisrun time

Mathematics Subject Classification ID

Related Items (3)

Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ Efficient Verified Implementation of Introsort and Pdqsort ⋮ For a few dollars more. Verified fine-grained algorithm analysis down to LLVM

Uses Software

• Edmonds-Karp
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Verifying asymptotic time complexity of imperative programs in Isabelle
• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Verified model checking of timed automata
• Formalizing the Edmonds-Karp Algorithm
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Refinement to Imperative/HOL
• Imperative Functional Programming with Isabelle/HOL
• Amortised Resource Analysis with Separation Logic
• Characteristic formulae for the verification of imperative programs

This page was built for publication: