VMCAI 2026
Mon 12 - Tue 13 January 2026 Rennes, France
co-located with POPL 2026
Mon 12 Jan 2026 11:30 - 12:00 at Horizons - Analysis 2 Chair(s): Benoît Montagu

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 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

11:00 - 12:30
Analysis 2VMCAI 2026 at Horizons
Chair(s): Benoît Montagu Inria
11:00
30m
Talk
Data Race Detection by Digest-Driven Abstract Interpretation
VMCAI 2026
Michael Schwarz National University of Singapore, Julian Erhard TU Munich; LMU Munich
Pre-print
11:30
30m
Talk
Termination Resilience Static Analysis
VMCAI 2026
Naïm Moussaoui Remil Inria & ENS | PSL, Paris, France, Caterina Urban Inria Paris - ENS - Université PSL
12:00
30m
Talk
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