Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming (Extended Version)
TL;DR
A novel hybrid approach that systematically derives upper bounds for the worst-case resource consumption of functional programs by combines dynamic symbolic execution to exhaustively explore all possible computation paths within a constrained input space with mixed-integer linear programming to derive empirically sound upper bounds.
Abstract
Existing approaches to resource analysis of programs can be classified into two main paradigms: static analysis and dynamic analysis methods. The former allow for formal guarantees but are inherently incomplete; the latter are widely applicable but may miss rare but characteristic (worst-case) scenarios and thus lack soundness. Hybrid approaches attempt to combine the strengths of both paradigms, thereby enabling the analysis of programs that are either too complex for purely static techniques or where dynamic approaches suffer from combinatorial explosion. In this paper, we present a novel hybrid approach that systematically derives upper bounds for the worst-case resource consumption of functional programs. Our method combines dynamic symbolic execution to exhaustively explore all possible computation paths within a constrained input space with mixed-integer linear programming to derive empirically sound upper bounds. We have implemented the methodology in a prototype tool, dubbed CompAS, which we made available on Zenodo.