Termination Resilience Static Analysis
summary
Claims an abstract-interpretation framework that proves absence of robust non-termination by computing piecewise ranking functions backward over a decision-tree domain that distinguishes untrusted inputs from internal choices. Extends Cousot-style ranking derivation and Urban & Miné’s decision-tree domain, implements a prototype analyzer row function as open source, and runs on SV-COMP and real-world modeled benchmarks, classifying over 65% of classical non-termination alarms as less critical (i.e., termination resilient).
AI-written summary · about
chapters (11)
- 0:00Termination resilience static analysis
- 2:14Robust non-termination and critical bugs
- 4:21Termination resilience as nondeterminism
- 5:03Concrete semantics and ranking functions
- 8:39Abstract semantics and soundness
- 10:50Static analysis with decision trees
- 16:50Resilient join for internal choices
- 18:12Prototype analyzer assumptions
- 19:57Related works and reachability
- 21:45Conclusion and future research
- 23:10Q&A
related talks
19mMechanized Logical Relations for Termination-Insensitive Noninterference
23mSecurity Reasoning via Substructural Dependency Tracking
19mDecompiling for Constant-Time Analysis
22mReconciling Progress-Intensive Noninterference and Declassification
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...
19mInference of Robust Reachability Constraints
20mTaking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses
32mSymbolic analysis by using folding narrowing with irreducibility and SMT constra...