For a few dollars more. Verified fine-grained algorithm analysis down to LLVM

DOI10.1007/978-3-030-72019-3_11zbMath1473.68222OpenAlexW3136814465MaRDI QIDQ2233462

Maximilian P. L. Haslbeck, Peter Lammich

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-72019-3_11

zbMATH Keywords

refinementalgorithm analysisprogram verification

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Searching and sorting (68P10) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Flexible Correct-by-Construction Programming

Uses Software

• HOL
• TiML
• Separation Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Refinement to imperative HOL
• Verifying asymptotic time complexity of imperative programs in Isabelle
• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Mechanized semantics for the clight subset of the C language
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Refinement to Imperative/HOL
• Amortised Resource Analysis with Separation Logic
• Comprehending monads
• Efficient Verified Implementation of Introsort and Pdqsort
• Containment control of a class of heterogeneous nonlinear multi-agent systems

This page was built for publication: For a few dollars more. Verified fine-grained algorithm analysis down to LLVM