Deciding Asynchronous Hyperproperties for Recursive Programs
summary
Paper introduces a new asynchronous hyperlogic that adds fixpoints, non-atomic tests (trace formulas with CARET-style call/return inspection), and a simpler mumbling jump criterion that advances to the next position where a single formula holds. Model checking stays decidable with the same finite-state complexity as related work, the paper proves mumbling is strictly more expressive than stuttering in the LTL-only setting, and gives the first pushdown model checking algorithm under a well-aligned restriction (no implementation yet).
AI-written summary · about
chapters (6)
- 0:00Introduction
- 2:24Motivation for new logic
- 7:20Mumbling Hμ features
- 11:38Pushdown model checking
- 13:47Conclusion
- 14:30Q&A
related talks
15mProducts of Recursive Programs for Hypersafety Verification
28mReasoning about Distributed Reconfigurable Systems
27mRecurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
26mKater: Automating Weak Memory Model Metatheory and Consistency Checking
25mProperty-agnostic base case extension for scalable verification of distributed systems
15mStatically Verified Refinements for Multiparty Protocols
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata