This program is tentative and subject to change.

Wed 4 Jun 2025 11:00 - 11:30 at S 9 - Testing and Debugging

In this paper, we present the design of Owi, a symbolic interpreter for WebAssembly written in OCaml, and how we used it to create a state-of-the-art tool to find bugs in programs combining C and Rust code. WebAssembly (Wasm) is a binary format for executable programs. Originally intended for web applications, Wasm is also considered a serious alternative for server-side runtimes and embedded systems due to its performance and security benefits. Despite its security guarantees and sandboxing capabilities, Wasm code is still vulnerable to buffer overflows and memory leaks, which can lead to exploits on production software. To help prevent those, different techniques can be used, including symbolic execution.

Owi is built around a modular, monadic interpreter capable of both normal and symbolic execution of Wasm programs. Monads have been identified as a way to write modular interpreters since 1995 and this strategy has allowed us to build a robust and performant symbolic execution tool which our evaluation shows to be the best currently available for Wasm. Moreover, because WebAssembly is a compilation target for multiple languages (such as Rust and C), Owi can be used to find bugs in C and Rust code, as well as in codebases mixing the two. We demonstrate this flexibility through illustrative examples and evaluate its scalability via comprehensive experiments using the 2024 Test-Comp benchmarks. Results show that Owi achieves comparable performance to state-of-the-art tools like KLEE and Symbiotic, and exhibits advantages in specific scenarios where KLEE’s approximations could lead to false negatives.

This program is tentative and subject to change.

Wed 4 Jun

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

10:30 - 12:00
Testing and DebuggingResearch Papers at S 9
10:30
30m
Talk
Dynamic Program Slices Change How Developers Diagnose Gradual Run-time Type Errors
Research Papers
Felipe Bañados Schwerter University of British Columbia, Ronald Garcia University of British Columbia, Reid Holmes University of British Columbia, Karim Ali NYU Abu Dhabi
11:00
30m
Talk
Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly
Research Papers
Léo Andrès LMF, OCamlPro, Filipe Marques INESC-ID; Instituto Superior Técnico - University of Lisbon, Arthur Carcano OCamlPro, Pierre Chambart OCamlPRO, José Fragoso Santos INESC-ID; Instituto Superior Técnico - University of Lisbon, Jean-Christophe Filliatre CNRS
11:30
30m
Talk
PolyDebug: a Framework for Polyglot Debugging
Research Papers
Philémon Houdaille DIVERSE Team, IRISA-INRIA, CNRS, Université Rennes 1, Djamel Eddine Khelladi CNRS, IRISA, University of Rennes, Benoit Combemale University of Rennes, Inria, CNRS, IRISA, Gunter Mussbacher McGill University, Tijs van der Storm CWI & University of Groningen