Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applic
summary
Presents a new stateful DPOR algorithm that is sound for non-terminating, event-driven programs by adding a novel termination criterion, computing conflicts per memory location, and performing a backward DFS on a state-transition graph to add backtrack points on previously discovered paths. Implements the technique in IoTCheck and runs 535 smart‑home app pairs (32 GB, 2 h); 300 pairs finish under at least one mode, DPOR lets 69 previously unfinished pairs finish and gives a 7× geometric-mean speedup, with two workloads where DPOR increases exploration.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:35Interaction of Smart Apps
- 3:20State-of-the-Art
- 5:17Outline
- 5:52Challenges and Techniques • Challenge #1: Premature Termination
- 9:48Challenges and Techniques • Challenge #2: Events as Transitions
- 20:55Algorithm: Running Example
related talks
20mTruly Stateless, Optimal Dynamic Partial Order Reduction
21mModel Checking C/C++ with Mixed-Size Accesses
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
54mReasoning about Progress of Concurrent Objects
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
23mVerifying Observational Robustness Against a C11-style Memory Model