Certified complexity (CerCo)

DOI10.1007/978-3-319-12466-7_1MaRDI QIDQ3460499zbMATH OpenOpenAlexFDO

Authors Roberto M. Amadio, Nicolas Ayache, François Bobot, Jaap P. Boender, Brian A. Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, Paolo Tranquilli

Publication date 7 January 2016

Published in Foundational and Practical Aspects of Resource Analysis (Search for Journal in Brave)

Full work available at URL https://www.pure.ed.ac.uk/ws/files/17744654/fopara13_author_final.pdf

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Theory of software (68N99) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Certifying compilation and run-time code generation
• Certified Static Analysis by Abstract Interpretation
• FM 2005: Formal Methods
• A formally verified compiler back-end

Cited in

(7)

• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• The verified CakeML compiler backend
• Indexed labels for loop iteration dependent costs
• Resource bound certification
• The query complexity of certification
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

This page was built for publication: Certified complexity (CerCo)

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