pith. machine review for the scientific record. sign in

arxiv: 2604.23035 · v2 · submitted 2026-04-24 · 💻 cs.PL

Recognition: unknown

Remote Concolic Multiverse Debugging -- Extended Version with Additional Appendices

Maarten Steevens , Tom Lauwaerts , Christophe Scholliers
Authors on Pith no claims yet

Pith reviewed 2026-05-08 08:34 UTC · model grok-4.3

classification 💻 cs.PL
keywords multiverse debuggingconcolic executionstate space reductionmicrocontroller debuggingnondeterministic programstrace-based debuggingremote debuggingWebAssembly
0
0 comments X

The pith

Interleaving concolic analysis with live debugging identifies input values for unique paths and prunes redundant states in microcontroller multiverse exploration.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Debugging nondeterministic programs on microcontrollers is difficult because external inputs create unpredictable execution paths that traditional tools cannot fully capture or reproduce. This paper develops a trace-based multiverse debugger that interleaves concolic execution during live sessions to select only those inputs producing distinct behaviors. The method prunes paths that repeat prior executions while still visiting every line of code. It replaces heavy snapshot storage with lighter traces, cutting memory use and communication costs compared with earlier snapshot-based debuggers. The prototype runs on the WARDuino WebAssembly virtual machine and shows smaller state spaces than standard multiverse approaches in real hardware tests.

Core claim

The paper presents a remote concolic multiverse debugger whose central technique interleaves concolic analysis with ongoing debugging sessions. Concolic execution determines the input values that generate distinct program paths; paths sharing the same inputs are discarded. This pruning occurs on-the-fly using program traces rather than full state snapshots, ensuring complete code coverage without exhaustive enumeration of every possible execution. The approach is shown to lower both state-space size and resource demands relative to prior multiverse debuggers for microcontrollers.

What carries the argument

The trace-based multiverse debugger that interleaves concolic analysis to identify input values defining unique program paths and thereby prunes the state space.

If this is right

  • Multiverse debugging becomes practical for resource-constrained microcontrollers that receive unpredictable sensor data.
  • Developers obtain full code coverage while examining far fewer execution states than exhaustive exploration requires.
  • Memory and communication overhead drop because traces replace full program snapshots.
  • Remote debugging sessions remain responsive even when external inputs create high nondeterminism.
  • The same pruning logic applies directly to other nondeterministic programs running on similar embedded platforms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The pruning technique might extend naturally to concurrent or distributed embedded systems that share similar input nondeterminism.
  • Combining the method with hardware-in-the-loop simulation could allow early debugging without physical devices.
  • Automated test-case generators could reuse the identified unique-path inputs to focus coverage on unexplored branches.
  • The trace representation may support post-hoc replay of only the retained paths for offline analysis.

Load-bearing premise

Concolic execution can correctly detect and discard only redundant paths in actual microcontroller hardware without overlooking critical behaviors or imposing excessive memory, communication, or time costs.

What would settle it

A controlled test in which a known bug is triggered only by a sensor-input sequence that the concolic pruner discards, or in which the reported state-space size fails to shrink on a program whose inputs produce many overlapping paths.

read the original abstract

Debugging nondeterministic programs is inherently difficult, particularly in microcontroller environments where execution paths can diverge unpredictably due to external sensor inputs. Traditional debugging techniques often fail to capture or reproduce this nondeterministic behavior effectively. Multiverse debugging has emerged as a compelling technique to debug nondeterministic programs, allowing developers to systematically explore all possible execution paths. Unfortunately, current multiverse debuggers are snapshot-based and most operate over a model of the program, limiting their use for debugging resource-constrained microcontrollers. Additionally, current multiverse debuggers, even ones specifically designed for microcontrollers suffer from state explosion making the state space overwhelming during debugging. To address these challenges, we introduce a trace-based multiverse debugger with a novel state-space reduction technique based on concolic execution. Our approach interleaves concolic analysis with live debugging to identify input values that define unique program paths. This hybrid technique efficiently prunes redundant paths from the state space while ensuring full code coverage. Unlike MIO, a recently published multiverse debugger for microcontrollers that focuses on IO consistency, our approach directly targets state explosion by leveraging concolic execution and uses a trace-based approach, significantly reducing the memory and communication overhead. We implemented a prototype using the WARDuino WebAssembly VM, demonstrating the feasibility and efficiency of our approach in real-world scenarios. Our results highlight substantial reductions in the state space compared to traditional multiverse debugging. This makes multiverse debugging more accessible and efficient for developers working with complex, nondeterministic programs running on microcontrollers.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper claims to introduce a trace-based multiverse debugger for nondeterministic microcontroller programs. It interleaves concolic analysis with live debugging to identify input-defined unique paths, pruning redundant paths while ensuring full code coverage. The approach is implemented in a WARDuino WebAssembly VM prototype and is positioned as reducing memory/communication overhead relative to snapshot-based methods such as MIO.

Significance. If the central claims of substantial state-space reduction and guaranteed coverage are substantiated, the technique could make multiverse debugging practical for resource-constrained embedded systems by mitigating state explosion in the presence of sensor-induced nondeterminism.

major comments (2)
  1. [Abstract] Abstract: the claims of 'substantial reductions in the state space' and 'full code coverage' are presented without any quantitative benchmarks, performance metrics, error bars, experimental methodology, or results tables to support them.
  2. [Abstract] Abstract: the soundness of concolic path pruning under microcontroller nondeterminism is not established; no completeness argument, proof, or exhaustive enumeration on a nondeterministic benchmark is supplied to show that all feasible paths under real sensor variation are preserved.
minor comments (1)
  1. The title refers to an 'Extended Version with Additional Appendices,' but the manuscript does not indicate the location or content of these appendices.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on our manuscript. We agree that the abstract would benefit from more explicit support for its claims and that a clearer treatment of soundness would strengthen the presentation. We respond to each major comment below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claims of 'substantial reductions in the state space' and 'full code coverage' are presented without any quantitative benchmarks, performance metrics, error bars, experimental methodology, or results tables to support them.

    Authors: The abstract is a high-level summary; the full manuscript contains an experimental evaluation section with quantitative benchmarks, state-space reduction metrics, coverage results, and methodology details comparing against snapshot-based approaches. We acknowledge that the abstract's claims would be more persuasive if accompanied by key quantitative highlights. In the revised version we will update the abstract to incorporate specific results from our evaluation (e.g., observed state-space reductions and coverage percentages) while respecting length constraints. revision: yes

  2. Referee: [Abstract] Abstract: the soundness of concolic path pruning under microcontroller nondeterminism is not established; no completeness argument, proof, or exhaustive enumeration on a nondeterministic benchmark is supplied to show that all feasible paths under real sensor variation are preserved.

    Authors: The manuscript explains that concolic analysis identifies input-defined unique paths and prunes only redundant ones while preserving coverage. We agree, however, that no formal completeness argument or exhaustive enumeration is currently supplied. We will add a soundness sketch (or appendix) in the revised version that argues, based on the exhaustive nature of concolic execution for the observed inputs, that all feasible sensor-induced paths are retained. revision: yes

Circularity Check

0 steps flagged

No circularity: purely descriptive engineering technique with no derivations or self-referential claims

full rationale

The paper presents a trace-based multiverse debugger that interleaves concolic analysis with live debugging to prune redundant paths while claiming full code coverage. No equations, parameters, uniqueness theorems, or derivation chains appear in the abstract or described approach. Claims rest on prototype implementation in WARDuino and reported state-space reductions rather than any mathematical reduction to inputs. No self-citations are invoked as load-bearing premises, and no ansatz or renaming of known results is used. The absence of any formal derivation makes circularity impossible by the defined criteria; the work is self-contained as an engineering proposal.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no equations, parameters, or formal model described.

pith-pipeline@v0.9.0 · 5578 in / 1133 out tokens · 50840 ms · 2026-05-08T08:34:12.639614+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 24 canonical work pages

  1. [1]

    1 IEEE Standard for Test Access Port and Boundary-Scan Architecture.IEEE Std 1149.1-2013 (Revision of IEEE Std 1149.1-2001), pages 1–444, May 2013.doi:10.1109/IEEESTD.2013. 6515989. 2 Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A Survey of Symbolic Execution Techniques.ACM Comput. Surv., 51(3):50:1–50:39, May ...

    work page doi:10.1109/ieeestd.2013 2013

  2. [2]

    6 Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt.Semantics Engineering with PLT Redex

    Association for Computing Machinery.doi:10.1145/1985793.1985995. 6 Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt.Semantics Engineering with PLT Redex. Mit Press,

    work page doi:10.1145/1985793.1985995

  3. [3]

    A debugging calculus for mobile ambients

    7 GianLuigi Ferrari and Emilio Tuosto. A debugging calculus for mobile ambients. InProceedings of the 2001 ACM Symposium on Applied Computing, Las Vegas Nevada USA, March

    2001

  4. [4]

    8 Jason Gait

    ACM.doi:10.1145/372202.380701. 8 Jason Gait. A probe effect in concurrent programs.Software: Practice and Experience, 16(3):225–233, 1986.doi:10.1002/spe.4380160304. 9 Patrice Godefroid. Model checking for programming languages using VeriSoft. InProceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, M. Steevens, T. La...

    work page doi:10.1145/372202.380701 1986

  5. [5]

    10 Patrice Godefroid, Nils Klarlund, and Koushik Sen

    Association for Computing Machinery.doi:10.1145/263699.263717. 10 Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: Directed automated random testing.SIGPLAN Not., 40(6):213–223, June 2005.doi:10.1145/1064978.1065036. 11 Robbert Gurdeep Singh.Taming Nondeterminism : Programming Language Abstractions and Tools for Dealing with Nondeterministic Progr...

    work page doi:10.1145/263699.263717 2005

  6. [6]

    13 Andreas Haas, Andreas Rossberg, Derek L

    doi: 10.4230/DARTS.5.2.4. 13 Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. Bringing the web up to speed with WebAssembly. InProceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 185–200, New York, NY, USA, June

    work page doi:10.4230/darts.5.2.4 2017

  7. [7]

    Schuff, Ben L

    Association for Computing Machinery.doi:10.1145/3062341.3062363. 14 Hubert Högl and Dominic Rath. Open on-chip debugger–openocd–.Fakultat fur Informatik, Tech. Rep,

    work page doi:10.1145/3062341.3062363

  8. [8]

    Ab- stract Debuggers: Exploring Program Behaviors using Static Analysis Results

    15 Karoliine Holter, Juhan Oskar Hennoste, Patrick Lam, Simmo Saan, and Vesal Vojdani. Ab- stract Debuggers: Exploring Program Behaviors using Static Analysis Results. InProceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! ’24, pages 130–146, New York, NY, USA, October

    2024

  9. [9]

    16 Ranjit Jhala and Rupak Majumdar

    Association for Computing Machinery.doi:10.1145/3689492.3690053. 16 Ranjit Jhala and Rupak Majumdar. Software model checking.ACM Comput. Surv., 41(4):21:1– 21:54, October 2009.doi:10.1145/1592434.1592438. 17 Vineet Kahlon, Chao Wang, and Aarti Gupta. Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In Ahmed Bouajja...

    work page doi:10.1145/3689492.3690053 2009

  10. [10]

    doi:10.1007/978-3-642-02658-4_31

    Springer. doi:10.1007/978-3-642-02658-4_31. 18 Mary Beth Kery, Amber Horvath, and Brad Myers. Variolite: Supporting Exploratory Programming by Data Scientists. InProceedings of the 2017 CHI Conference on Human Factors in Computing Systems, CHI ’17, pages 1265–1276, New York, NY, USA, May

    work page doi:10.1007/978-3-642-02658-4_31 2017

  11. [11]

    19 Mary Beth Kery and Brad A

    Association for Computing Machinery.doi:10.1145/3025453.3025626. 19 Mary Beth Kery and Brad A. Myers. Exploring exploratory programming. In2017 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC), pages 25–29, October 2017.doi:10.1109/VLHCC.2017.8103446. 20 Muhammad Zahid Khan, Bob Askwith, Faycal Bouhafs, and Muhammad Asim. Limitation...

    work page doi:10.1145/3025453.3025626 2017

  12. [12]

    21 James C

    IEEE.doi:10.1109/WAINA.2011.59. 21 James C. King. Symbolic execution and program testing.Communications of the ACM, 19(7):385–394, July 1976.doi:10.1145/360248.360252. 22 R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün. Static partial order reduction. In Bernhard Steffen, editor,Tools and Algorithms for the Construction and Analysis of Systems, p...

    work page doi:10.1109/waina.2011.59 2011

  13. [13]

    23 Tom Lauwaerts, Carlos Rojas Castillo, Robbert Gurdeep Singh, Matteo Marra, Christophe Scholliers, and Elisa Gonzalez Boix

    Springer.doi:10.1007/BFb0054182. 23 Tom Lauwaerts, Carlos Rojas Castillo, Robbert Gurdeep Singh, Matteo Marra, Christophe Scholliers, and Elisa Gonzalez Boix. Event-Based Out-of-Place Debugging. InProceedings of the 19th International Conference on Managed Programming Languages and Runtimes, MPLR ’22, pages 85–97, New York, NY, USA, November

    work page doi:10.1007/bfb0054182

  14. [14]

    24 Tom Lauwaerts, Robbert Gurdeep Singh, and Christophe Scholliers

    Association for Computing Machinery.doi:10.1145/3546918.3546920. 24 Tom Lauwaerts, Robbert Gurdeep Singh, and Christophe Scholliers. WARDuino: An embedded WebAssembly virtual machine.Journal of Computer Languages, page 101268, February

    work page doi:10.1145/3546918.3546920

  15. [15]

    28 RemoteConcolicMultiverseDebugging: ExtendedVersionwithAdditionalAppendices 25 Tom Lauwaerts, Maarten Steevens, and Christophe Scholliers

    doi:10.1016/j.cola.2024.101268. 28 RemoteConcolicMultiverseDebugging: ExtendedVersionwithAdditionalAppendices 25 Tom Lauwaerts, Maarten Steevens, and Christophe Scholliers. MIO: Multiverse Debugging in the Face of Input/Output.Proc. ACM Program. Lang., 9(OOPSLA2), October

    work page doi:10.1016/j.cola.2024.101268 2024

  16. [16]

    26 Chao Li, Rui Chen, Boxiang Wang, Zhixuan Wang, Tingting Yu, Yunsong Jiang, Bin Gu, and Mengfei Yang

    doi:10.1145/3763136. 26 Chao Li, Rui Chen, Boxiang Wang, Zhixuan Wang, Tingting Yu, Yunsong Jiang, Bin Gu, and Mengfei Yang. An Empirical Study on Concurrency Bugs in Interrupt-Driven Embedded Software. InProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 1345–1356. ACM. URL:https://dl.acm.org/doi/10.1145/ ...

    work page doi:10.1145/3763136

  17. [17]

    Pycg: Practical call graph generation in python,

    doi:10.1109/ICSE43902.2021.00051. 28 Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão. Concolic Execution for WebAssembly. In Karim Ali and Jan Vitek, editors,36th European Conference on Object- Oriented Programming (ECOOP 2022), volume 222 ofLeibniz International Proceedings in Informatics (LIPIcs ), pages 11:1–11:29, Dagstuhl, Germany,

    work page doi:10.1109/icse43902.2021.00051 2021

  18. [18]

    29 Matteo Marra, Guillermo Polito, and Elisa Gonzalez Boix

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik.doi:10.4230/LIPIcs.ECOOP.2022.11. 29 Matteo Marra, Guillermo Polito, and Elisa Gonzalez Boix. Out-Of-Place debugging: A debugging architecture to reduce debugging interference.The Art, Science, and Engineering of Programming, 3(2):3:1–3:29, November 2018.doi:10.22152/programming-journal.org/ 2019/3/3. 30 C...

    work page doi:10.4230/lipics.ecoop.2022.11 2022

  19. [19]

    doi:10.1145/3623476.3623526

    Association for Computing Machinery. doi:10.1145/3623476.3623526. 33 Matthias Pasquier, Ciprian Teodorov, Frédéric Jouault, Matthias Brun, Luka Le Roux, and Loïc Lagadec. Practical multiverse debugging through user-defined reductions: Application to UML models. InProceedings of the 25th International Conference on Model Driven Engineering Languages and Sy...

    work page doi:10.1145/3623476.3623526

  20. [20]

    34 Michael Perscheid, Benjamin Siegmund, Marcel Taeumel, and Robert Hirschfeld

    Association for Computing Machinery.doi:10.1145/3550355.3552447. 34 Michael Perscheid, Benjamin Siegmund, Marcel Taeumel, and Robert Hirschfeld. Studying the advancement in debugging practice of professional software developers.Software Quality Journal, 25(1):83–110, March 2017.doi:10.1007/s11219-015-9294-2. 35 Albert Pötsch, Florian Haslhofer, and Andrea...

    work page doi:10.1145/3550355.3552447 2017

  21. [21]

    36 Jonathan B

    Association for Computing Machinery.doi:10.1145/3131542.3140259. 36 Jonathan B. Rosenberg.How Debuggers Work: Algorithms, Data Structures, and Architecture. John Wiley & Sons, Inc., USA, October

    work page doi:10.1145/3131542.3140259

  22. [22]

    37 Tamás Roska. Limitations and complexity of digital hardware simulators used for large- scale analogue circuit and system dynamics.International Journal of Circuit Theory and Applications, 18(1):11–21, 1990.doi:10.1002/cta.4490180104. 38 Koushik Sen and Gul Agha. Automated Systematic Testing of Open Distributed Programs. In Luciano Baresi and Reiko Heck...

    work page doi:10.1002/cta.4490180104 1990

  23. [23]

    Springer.doi:10.1007/11693017_25. M. Steevens, T. Lauwaerts, and C. Scholliers 29 39 Gašper Skvarč Božič, Ibai Irigoyen Ceberio, and Albrecht Mayer. In-Field Debugging of Automotive Microcontrollers for Highest System Availability. InProceedings of the 2nd ACM International Workshop on Future Debugging Techniques, DEBT 2024, pages 2–8, New York, NY, USA, ...

    work page doi:10.1007/11693017_25 2024

  24. [24]

    Association for Computing Machinery.doi:10.1145/3678720. 3685314. 40 Karl Söderby and Ubi De Feo. Debugging with the arduino IDE 2.0. https://docs.arduino.cc/software/ide-v2/tutorials/ide-v2-debugger, November

    work page doi:10.1145/3678720

  25. [25]

    Sangho Suh, Bryan Min, Srishti Palani, and Haijun Xia

    41 Sara Steegen, Francis Tuerlinckx, Andrew Gelman, and Wolf Vanpaemel. Increasing Trans- parency Through a Multiverse Analysis.Perspectives on Psychological Science, 11(5):702–712, September 2016.doi:10.1177/1745691616658637. 42 Bastian Steinert, Damien Cassou, and Robert Hirschfeld. CoExist: Overcoming aversion to change.SIGPLAN Not., 48(2):107–118, Oct...

    work page doi:10.1177/1745691616658637 2016

  26. [26]

    44 Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers

    Association for Computing Machinery.doi:10.1145/3141834.3141839. 44 Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers. Multiverse Debugging: Non-Deterministic Debug- ging for Non-Deterministic Programs (Brave New Idea Paper). InDROPS- IDN/v2/Document/10.4230/LIPIcs.ECOOP.2019.27. Schloss Dagstuhl – Lei...

    work page doi:10.1145/3141834.3141839 2019

  27. [27]

    env", "chip_delay

    This is example is a modification from the original arduino-while (Source) example program with the calibration step removed. Just like the other arduino examples the source code was also translated into AssemblyScript for use on the WARDuino VM. 1@external("env", "chip_delay") declarefunctionchip_delay(value: i32): void; 2@external("env", "chip_pin_mode"...

    2048