Termination Resilience Static Analysis
We present a novel abstract interpretation-based static analysis framework for proving Termination Resilience, the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an untrusted (e.g., externally-controlled) input can force infinite execution, independently of other trusted (e.g., controlled) variables. Our framework is a semantic generalization of Cousot and Cousot’s abstract interpretation-based ranking function derivation, and our sound static analysis extends Urban and Miné’s decision tree abstract domain in a non-trivial way to manage the distinction between untrusted and trusted program variables. Our approach is implemented in an open-source tool and evaluated on bench- marks sourced from SV-COMP and modeled after real-world software, demonstrating practical effectiveness in verifying Termination Resilience and detecting potential Robust Non-Termination vulnerabilities.
Mon 12 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 30mTalk | Data Race Detection by Digest-Driven Abstract Interpretation VMCAI 2026 Pre-print | ||
11:30 30mTalk | Termination Resilience Static Analysis VMCAI 2026 Naïm Moussaoui Remil Inria & ENS | PSL, Paris, France, Caterina Urban Inria Paris - ENS - Université PSL | ||
12:00 30mTalk | Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification VMCAI 2026 Andreas Lindner Uppsala universitet, Karl Palmskog KTH Royal Institute of Technology, Scott Constable Intel Corporation, Mads Dam KTH, Roberto Guanciale KTH Royal Institute of Technology, Hamed Nemati KTH Royal Institute of Technology | ||