Complexity verification using guided theorem enumeration

DOI10.1145/3009837.3009864MaRDI QIDQ5370898zbMATH OpenOpenAlexWikidataFDO

Authors Akhilesh Srikanth, Burak Sahin, William R. Harris

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3009837.3009864

zbMATH Keywords

complexityinterpolationtheorem grounding

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• A framework for verification and debugging of resource usage properties: resource usage verification
• SPEED: precise and efficient static estimation of program computational complexity
• Automated resource analysis with Coq proof objects
• Theorem Proving in Higher Order Logics

Cited in

(4)

• Inferring expected runtimes of probabilistic integer programs using expected sizes
• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• Polynomial loops: beyond termination

Describes a project that uses

Uses Software

• Soot
• LeetCode
• CAMPY
• z3

This page was built for publication: Complexity verification using guided theorem enumeration

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