A Program Logic for Under-approximating Worst-case Resource Usage
Ziyue Jin, Di Wang
TL;DR
This paper addresses the challenge of under‑approximating worst‑case resource usage in programs, proposing a quantitative extension of Incorrectness Logic. It introduces three logics, QFUA, QBUA, and QBUA Diamond, to reason about high resource usage in a compositional and executable framework, with formal soundness and completeness proofs and a mechanized Rocq formalization. An OCaml prototype verifier demonstrates the approach on eight case studies, including password validation, insertion sort, quicksort with a stack, and a producer–consumer system, while a verification framework supports arrays and predicate transformers. The work provides a principled, scalable method for identifying high‑cost execution paths and under‑approximating worst‑case resource usage, complementing existing over‑approximate analyses and enabling targeted performance and security analyses in practice.
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.