Search papers, labs, and topics across Lattice.
This paper introduces a novel hybrid approach that leverages dynamic symbolic execution and mixed-integer linear programming to derive upper bounds for the worst-case resource consumption of functional programs. By systematically exploring all possible computation paths within a constrained input space, the method addresses the limitations of both static and dynamic analysis techniques, providing a more robust solution for complex program analysis. The implementation of this approach in the prototype tool CompAS demonstrates its effectiveness in generating empirically sound resource bounds, making it a significant advancement in resource analysis methodologies.
A hybrid method combining symbolic execution and linear programming reveals sound upper bounds for resource consumption, overcoming the limitations of traditional analysis techniques.
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.
