Amortised resource analysis with separation logic

DOI10.1007/978-3-642-11957-6_6MaRDI QIDQ3558217zbMATH OpenOpenAlexFDO

Authors Robert Atkey

Publication date 4 May 2010

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-11957-6_6

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05)

Recommendations

• Type-based amortized resource analysis with integers and arrays
• Type-based amortized resource analysis with integers and arrays
• Amortised resource analysis for object-oriented programs
• Theorem Proving in Higher Order Logics
• Multivariate amortized resource analysis

Cited in

(17)

• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Selectively-amortized resource bounding
• For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
• A Hoare logic for energy consumption analysis
• Reasoning about resources in the embedded systems language Hume
• Relational cost analysis in a functional-imperative setting
• Bringing Order to the Separation Logic Jungle
• Verified Root-Balanced Trees
• Denotational semantics as a foundation for cost recurrence extraction for functional languages
• scientific article; zbMATH DE number 7204445 (Why is no real title available?)
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• Two decades of automatic amortized resource analysis
• Resource separation in dynamic logic of propositional assignments
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Amortized complexity verified

Describes a project that uses

Uses Software

• Coq
• COSTA
• SPEED

This page was built for publication: Amortised resource analysis with separation logic

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