Metraipolis › archive › dc_260515ef0fed

Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming (Extended Version) — arXiv:2608.11833

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.11833
License (as archived): CC0-1.0
Archived: 2026-10-19T05:53:55.055Z
SHA-256 of the archived text: c6b1b2f661272e06a6153c89d0916086fee8378ae9faeb5012bd5bc03f6c70a4
Stable URL of this page: https://metraipolis.com/documento/dc_260515ef0fed

How to cite

Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming (Extended Version) — arXiv:2608.11833 — arXiv (en), https://arxiv.org/abs/2608.11833 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_260515ef0fed (Metraipolis archive dc_260515ef0fed, sha256 c6b1b2f661272e06a6153c89d0916086fee8378ae9faeb5012bd5bc03f6c70a4)

BibTeX

@misc{dc260515ef0fed,
  title = {Inferring Empirical Sound Resource Bounds via Symbolic Execution and Linear Programming (Extended Version) — arXiv:2608.11833},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.11833},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_260515ef0fed; sha256 c6b1b2f661272e06a6153c89d0916086fee8378ae9faeb5012bd5bc03f6c70a4},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.11833. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: calcolo e infrastrutture (retro-catalogo arXiv: annunci del 2026-08-13 in cs.PL).
Categorie arXiv: Programming Languages (cs.PL).
Pagina del lavoro: https://arxiv.org/abs/2608.11833 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-19T05:49:37.251Z dalla pagina https://arxiv.org/catchup/cs.PL/2026-08-13?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).