A Program Logic for Under-approximating Worst-case Resource Usage

TL;DR

This paper introduces a novel program logic that under-approximates worst-case resource usage, providing more precise analysis of high-resource-consuming execution paths with formal guarantees.

Contribution

It adapts incorrectness logic to quantitatively reason about resource consumption, including high-water mark analysis, with formal soundness, completeness, and a verified prototype.

Findings

Logic is sound and complete for a simple IMP-like language.

Prototype checker successfully analyzes resource usage in case studies.

Supports reasoning about high-water marks in resource consumption.

Abstract

Understanding and predicting the worst-case resource usage is crucial for software quality; however, existing methods either over-approximate with potentially loose bounds or under-approximate without asymptotic guarantees. This paper presents a program logic to under-approximate worst-case resource usage, adapting incorrectness logic (IL) to reason quantitatively about resource consumption. We propose quantitative forward and backward under-approximate (QFUA and QBUA) triples, which generalize IL to identify execution paths leading to high resource usage. We also introduce a variant of QBUA that supports reasoning about high-water marks. Our logic is proven sound and complete with respect to a simple IMP-like language, and all meta-theoretical results are mechanized and verified in Rocq. We implement a prototype checker for all three variants of our logic and demonstrate its utility through a few examples and four case studies.