A Navigation Logic for Recursive Programs with Dynamic Thread Creation
summary
Defines NTL, a temporal logic for Dynamic Pushdown Networks that adds spawn and caller modalities to navigate thread-creation and call/return structure, encodes models as execution graphs turned into trees by dropping return edges, and reduces model checking to emptiness of two-way alternating parity tree automata. Shows model checking and satisfiability are XTime-complete, with complexity exponential only in formula size and polynomial in model size, and proves greater expressiveness than single-thread LTL.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:23Formal model requirements
- 3:13Execution graphs for DPNs
- 6:20Limitations of LTL for DPNs
- 7:46NTL introduction
- 10:21Example properties in NTL
- 13:11Model checking for NTL
- 16:47Complexity vs LTL
- 17:08Future work
- 17:30Q&A
related talks
24mAn Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on(…)
24mA Concurrent Program Logic with a Future and History
26mContext-Bounded Verification of Liveness for Multithreaded Shared-Memory Programs
29mAutomata-Driven Partial Order Reduction and Guided Search for LTL Model Checking
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
25mParametrised Verification of Intel-x86 Programs
28mCAAT: Consistency as a Theory
22mContext-Bounded Verification of Thread Pools