Selectively-amortized resource bounding
From MaRDI portal
Publication:2145338
DOI10.1007/978-3-030-88806-0_14zbMATH Open1497.68117arXiv2108.08263OpenAlexW3209554355MaRDI QIDQ2145338FDOQ2145338
Authors: Tianhan Lu, Bor-Yuh Evan Chang, Ashutosh Trivedi 
Publication date: 17 June 2022
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.
Full work available at URL: https://arxiv.org/abs/2108.08263
Recommendations
Cites Work
- Multivariate amortized resource analysis
- Synthesis of Circular Compositional Program Proofs via Abduction
- Computer Aided Verification
- Program Slicing
- Completing the temporal picture
- SPEED
- Amortized Computational Complexity
- Automated resource analysis with Coq proof objects
- Amortised resource analysis with separation logic
- Towards automatic resource bound analysis for OCaml
- More precise yet widely applicable cost analysis
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- Complexity and resource bound analysis of imperative programs using difference constraints
- Polynomial Invariants for Affine Programs
- Type-directed bounding of collections in reactive programs
- Title not available (Why is that?)
Uses Software
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)
