Temporal Breakpoints for Multiverse Debugging
summary
Claim: adding temporal breakpoints lets a multiverse debugger reason over sets of executions, not just single traces, and it is practical. Implementation: a language-agnostic multiverse debugger extended in the AnimUML/ANL environment, formalized in Lean, with regular-expressions, statecharts, and Büchi automata breakpoint languages. Technique: lazy synchronous composition of subject and breakpoint automata, reuse of LTL→Büchi tooling, reductions for scalability, and witness-trace extraction for run-to-breakpoint queries. Outcome: a working prototype that finds accepting traces and isolates cyclic/infinite behaviors in nondeterministic models.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:41Motivation for temporal breakpoints
- 3:55Four breakpoint types
- 7:36Reusable debugging tools
- 10:02Modular debugger API design
- 13:16Run to breakpoint with temporal logic
- 16:09ANL tool integration & case studies
- 19:25Future directions & user studies
- 21:32Q&A
- 21:53Jump operations in debugging
- 23:38Case studies & language support
- 25:03Breakpoint automata power
- 28:01Closing remarks
related talks
37mThe Bright Future of Debuggers: Challenges and Opportunities
26mTime-awareness in Object-exploration Tools: Toward In Situ Omniscient Debugging
25mTime Travel Debuggers
24mGHC Plugin for Setting Breakpoints
01h 02mTime Travel Debugging
19mMultiverse Notebook: Shifting Data Scientists to Time Travelers
24mA Counterexample-Guided Debugger for Non-Recursive Datalog
26mTime travel debugging: A step-by-step guide