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.

翻译：理解和预测最坏情况资源使用量对于软件质量至关重要；然而，现有方法要么以可能宽松的界进行上近似，要么进行缺乏渐近保证的下近似。本文提出了一种用于下近似最坏情况资源使用量的程序逻辑，通过调整不正确性逻辑（IL）以对资源消耗进行定量推理。我们提出了定量前向与后向下近似（QFUA 和 QBUA）三元组，它们将 IL 推广以识别导致高资源使用的执行路径。我们还引入了一种支持推理高水位标记的 QBUA 变体。我们的逻辑相对于一种简单的类 IMP 语言被证明是可靠且完备的，所有元理论结果均在 Rocq 中实现机械化与验证。我们为逻辑的所有三种变体实现了一个原型检查器，并通过若干示例和四个案例研究展示了其实用性。