SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Fri 17 Oct 2025 16:15 - 16:30 at Orchid Small - Debugging and Validation Chair(s): Stefan Marr

Debugging non-deterministic programs on microcontrollers is notoriously challenging, especially when bugs manifest in unpredictable, input-dependent execution paths. A recent approach, called multiverse debugging, makes it easier to debug non-deterministic programs by allowing programmers to explore all potential execution paths. Current multiverse debuggers enable both forward and backward traversal of program paths, and some facilitate jumping to any previously visited states, potentially branching into alternative execution paths within the state space.

Unfortunately, debugging programs that involve input/output operations using existing multiverse debuggers can reveal inaccessible program states, i.e. states which are not encountered during regular execution. This can significantly hinder the debugging process, as the programmer may spend substential time exploring and examining inaccessible program states, or worse, may mistakenly assume a bug is present in the code, when in fact, the issue is caused by the debugger.

This paper presents a novel approach to multiverse debugging, which can accommodate a broad spectrum of input/output operations. We provide the semantics of our approach and prove the correctness of our debugger, ensuring that despite having support for a wide range of input/output operations the debugger will only explore those program states which can be reached during regular execution.

We have developed a prototype, called MIO, leveraging the WARDuino WebAssembly virtual machine to demonstrate the feasibility and efficiency of our techniques. As a demonstration of the approach we highlight a color dial built with a Lego Mindstorms motor, and color sensor, providing a tangible example of how our approach enables multiverse debugging for programs running on a STM32 microcontroller.

Fri 17 Oct

Displayed time zone: Perth change

16:00 - 17:30
Debugging and ValidationOOPSLA at Orchid Small
Chair(s): Stefan Marr Johannes Kepler University Linz
16:00
15m
Talk
Debugging WebAssembly? Put some Whamm on it!
OOPSLA
Elizabeth Gilbert Carnegie Mellon University, Matthew Schneider Carnegie Mellon University, Zixi An , Suhas Thalanki Carnegie Mellon University, Wavid Bowman University of Florida, Alexander Bai New York University, Ben L. Titzer Carnegie Mellon University, Heather Miller Carnegie Mellon University and Two Sigma
Link to publication DOI Pre-print
16:15
15m
Talk
MIO: Multiverse Debugging in the face of Input/Output
OOPSLA
Tom Lauwaerts Universiteit Gent, Belgium, Maarten Steevens Ghent University, Belgium, Christophe Scholliers Universiteit Gent, Belgium
Link to publication DOI Pre-print
16:30
15m
Talk
PReMM: LLM-Based Program Repair for Multi-Method Bugs via Divide and Conquer
OOPSLA
Linna Xie Nanjing University, Zhong Li Nanjing University, Yu Pei Hong Kong Polytechnic University, Zhongzhen Wen Nanjing University, Kui Liu Huawei, Tian Zhang Nanjing University, Xuandong Li Nanjing University
16:45
15m
Talk
Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
OOPSLA
Ruixin Wang Purdue University, Zhongkai Zhao National University of Singapore, Le Fang Purdue University, Nan Jiang Purdue University, Yiling Lou University of Illinois at Urbana-Champaign, Lin Tan Purdue University, Tianyi Zhang Purdue University
Link to publication DOI Pre-print
17:00
15m
Talk
Translation Validation for LLVM's AArch64 Backend
OOPSLA
Ryan Berger Nvidia, Mitch Briles University of Utah, Nader Boushehrinejad Moradi University of Utah, Nicholas Coughlin Defence Science and Technology Group, Australia, Kait Lam Defence Science and Technology Group / School of EECS, University of Queensland, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon, Stefan Mada University of Utah, Tanmay Tirpankar University of Utah, John Regehr University of Utah
17:15
15m
Talk
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
OOPSLA
Maolin Sun Nanjing University, Yibiao Yang Nanjing University, Jiangchang Wu State Key Laboratory for Novel Software Technology, Nanjing University, Yuming Zhou Nanjing University