A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification

DOI10.1007/978-3-319-89884-1_19zbMath1418.68055OpenAlexW2798025005MaRDI QIDQ2323994

François Pottier, Arthur Charguéraud, Armaël Guéneau

Publication date: 13 September 2019

Full work available at URL: https://doi.org/10.1007/978-3-319-89884-1_19

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Synthesis with asymptotic resource bounds ⋮ Unnamed Item ⋮ Selectively-amortized resource bounding ⋮ Denotational semantics as a foundation for cost recurrence extraction for functional languages ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ For a few dollars more. Verified fine-grained algorithm analysis down to LLVM

This page was built for publication: A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification