Automated resource analysis with Coq proof objects

DOI10.1007/978-3-319-63390-9_4zbMath1494.68051OpenAlexW2735409225MaRDI QIDQ2164211

Zhong Shao, Quentin Carbonneaux, Jan Hoffmann, Thomas W. 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)

Related Items (6)

Selectively-amortized resource bounding ⋮ Unnamed Item ⋮ Amortized complexity verified ⋮ 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 ⋮ Two decades of automatic amortized resource analysis

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