Automated resource analysis with Coq proof objects

DOI10.1007/978-3-319-63390-9_4MaRDI QIDQ2164211zbMATH OpenOpenAlexFDO

Authors Quentin Carbonneaux, Jan Hoffmann, Zhong Shao, Thomas Reps

Publication date 12 August 2022

Full work available at URL https://doi.org/10.1007/978-3-319-63390-9_4

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Towards automatic resource bound analysis for OCaml
• Automatic inference of resource consumption bounds
• Type-based amortized resource analysis with integers and arrays
• Selectively-amortized resource bounding
• Type-based amortized resource analysis with integers and arrays

Cited in

(12)

• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Selectively-amortized resource bounding
• Automatic inference of resource consumption bounds
• Resource analysis driven by (conditional) termination proofs
• Complexity verification using guided theorem enumeration
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• Two decades of automatic amortized resource analysis
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
• Amortized complexity verified
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
• Polynomial loops: beyond termination

This page was built for publication: Automated resource analysis with Coq proof objects

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