Metraipolis › archive › dc_73bb03bfe403

Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots (Extended Version) — arXiv:2608.18327

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.18327
License (as archived): CC0-1.0
Archived: 2026-10-18T14:10:06.450Z
SHA-256 of the archived text: ea01649e3ab5fac7931fefe1238343924f0b417688d3a816ebd1b48c79747c8f
Stable URL of this page: https://metraipolis.com/documento/dc_73bb03bfe403

How to cite

Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots (Extended Version) — arXiv:2608.18327 — arXiv (en), https://arxiv.org/abs/2608.18327 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_73bb03bfe403 (Metraipolis archive dc_73bb03bfe403, sha256 ea01649e3ab5fac7931fefe1238343924f0b417688d3a816ebd1b48c79747c8f)

BibTeX

@misc{dc73bb03bfe403,
  title = {Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots (Extended Version) — arXiv:2608.18327},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.18327},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_73bb03bfe403; sha256 ea01649e3ab5fac7931fefe1238343924f0b417688d3a816ebd1b48c79747c8f},
  year = {2026}
}

Archived text

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

Concolic execution is a variant of symbolic execution that runs a program simultaneously with concrete and symbolic inputs. It records the symbolic constraints encountered along a concrete execution path, then solves those constraints to generate inputs that explore new paths. Existing concolic engines generally follow one of two implementation strategies: Interpreter-based systems are comparatively simple to build but incur substantial interpretation overhead, while instrumentation-based systems avoid this overhead but typically re-execute the program from the beginning for each new input. In this paper, we develop a new approach that achieves the best of both worlds. Starting from the concrete semantics of the target language, we first develop a definitional concolic interpreter and stage it to compile away interpretation overhead while retaining the simplicity of an interpretation-based implementation. By expressing the staged interpreter in continuation-passing style, we can capture execution snapshots at branch points and resume from them when exploring alternative paths, avoiding repeated execution from the program entry. Because snapshot-reuse can itself incur overhead, we further develop a heuristic that favors snapshot-reuse only when it is expected to be beneficial. We instantiate this approach for WebAssembly and implement it in a new concolic-execution compiler GenWasym. Across 184 benchmarks, GenWasym with staging alone achieves a $29.4\times$ average speedup over the interpreter-based WASP; heuristic snapshot-reuse further increases the speedup to $44.9\times$.

Tema degli esploratori: calcolo e infrastrutture (retro-catalogo arXiv: annunci del 2026-08-20 in cs.PL).
Categorie arXiv: Programming Languages (cs.PL).
Pagina del lavoro: https://arxiv.org/abs/2608.18327 — 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-18T14:08:50.611Z dalla pagina https://arxiv.org/catchup/cs.PL/2026-08-20?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).