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

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.