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

DOI10.1007/978-3-030-72019-3_11MaRDI QIDQ2233462zbMATH OpenOpenAlexFDO

Authors Maximilian P. L. Haslbeck, Peter Lammich

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

algorithm analysisprogram verificationrefinement

Mathematics Subject Classification ID

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

Recommendations

• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Refinements for free!
• Complexity verification using guided theorem enumeration
• Certified complexity (CerCo)
• FM 2005: Formal Methods

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
• Comprehending monads
• Containment control of a class of heterogeneous nonlinear multi-agent systems
• Efficient Verified Implementation of Introsort and Pdqsort
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• Mechanized semantics for the clight subset of the C language
• Refinement to imperative HOL
• Refinement to Imperative/HOL
• 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

(5)

• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Flexible Correct-by-Construction Programming
• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
• NREST: Nondeterministc RESult monad with Time
• van Emde Boas Trees

Describes a project that uses

Uses Software

• Separation Logic
• HOL
• TiML

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233462)