Stuttering for Free
summary
Presents FreeSim, a new stuttering-simulation technique mechanized in Coq that replaces the usual “synchronous progress” requirement with asynchronous progress, letting stuttering steps on each side accumulate and later combine. Claims propositionally equivalent power to prior simulations but strictly better usability, formalizes a concrete replayability property showing FreeSim can emulate and mix existing stuttering techniques, and demonstrates effectiveness on case studies including a CompCert metatheory simplification and extending ITrees with DTrees; artifacts are available and evaluated.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:21Behavior refinement
- 3:50Simulation limitations
- 6:16Asynchronous progress example
- 8:42FreeSim introduction
- 10:47FreeSim formal definition
- 11:49Why FreeSim is ultimate
- 13:54FreeSim applications
- 14:37Q&A
related talks
13mA Family of Languages for Trustworthy Agent-Based Simulation
17mA Co-Simulation Middleware: Virtual Testing of Automotive Applications with Multiple Simulators
27mLet's Bring System Dynamics Back to CS!
29mQ: A Sound Verification Framework for Statecharts and Their Implementations
19mPete's Footprints
27mActive DSU: Dynamic Software Updates for Active Functions
57mInvited Talk: Bridging Safety and Performance
24mQSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing