Selectively-amortized resource bounding

DOI10.1007/978-3-030-88806-0_14MaRDI QIDQ2145338zbMATH OpenOpenAlexFDO

Authors Tianhan Lu, Bor-Yuh Evan Chang, Ashutosh Trivedi

Publication date 17 June 2022

Full work available at URL https://arxiv.org/abs/2108.08263

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: We consider the problem of automatically proving resource bounds. That is, we study how to prove that an integer-valued resource variable is bounded by a given program expression. Automatic resource-bound analysis has recently received significant attention because of a number of important applications (e.g., detecting performance bugs, preventing algorithmic-complexity attacks, identifying side-channel vulnerabilities), where the focus has often been on developing precise amortized reasoning techniques to infer the most exact resource usage. While such innovations remain critical, we observe that fully precise amortization is not always necessary to prove a bound of interest. And in fact, by amortizing selectively, the needed supporting invariants can be simpler, making the invariant inference task more feasible and predictable. We present a framework for selectively-amortized analysis that mixes worst-case and amortized reasoning via a property decomposition and a program transformation. We show that proving bounds in any such decomposition yields a sound resource bound in the original program, and we give an algorithm for selecting a reasonable decomposition.

Recommendations

• Type-based amortized resource analysis with integers and arrays
• Type-based amortized resource analysis with integers and arrays
• Multivariate amortized resource analysis
• From Shapes to Amortized Complexity
• Towards automatic resource bound analysis for OCaml

Cites work

• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
• Amortised resource analysis with separation logic
• Amortized Computational Complexity
• Automated resource analysis with Coq proof objects
• Completing the temporal picture
• Complexity and resource bound analysis of imperative programs using difference constraints
• Computer Aided Verification
• More precise yet widely applicable cost analysis
• Multivariate amortized resource analysis
• Polynomial Invariants for Affine Programs
• Program Slicing
• SPEED: precise and efficient static estimation of program computational complexity
• Synthesis of circular compositional program proofs via abduction
• Towards automatic resource bound analysis for OCaml
• Type-directed bounding of collections in reactive programs

Cited in

(1)

• Automated resource analysis with Coq proof objects

Describes a project that uses

Uses Software

• z3

This page was built for publication: Selectively-amortized resource bounding

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