<figure><img src="image_1.png" /></figure>

HAL
open science

# Termination Resilience Static Analysis

Naïm Moussaoui Remil, Caterina Urban

► To cite this version:

Naïm Moussaoui Remil, Caterina Urban. Termination Resilience Static Analysis. VMCAI 2026 - 27th International Conference on Verification, Model Checking, and Abstract Interpretation, Jan 2026, Rennes, France. hal-05398150

HAL Id: hal-05398150

https://inria.hal.science/hal-05398150v1

Submitted on 4 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Termination Resilience Static Analysis

Naïm Moussaoui Remil and Caterina Urban

Inria & ENS | PSL, Paris, France
{naim.moussaoui-remil,caterina.urban}@inria.fr

<figure><img src="image_3.png" /></figure>

**Abstract.** 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 benchmarks sourced from SV-COMP and modeled after real-world software, demonstrating practical effectiveness in verifying Termination Resilience and detecting potential Robust Non-Termination vulnerabilities.

## 1 Introduction

Termination is one of the oldest and most fundamental properties of programs. Yet, in practice, requiring termination in every possible case can be unnecessarily restrictive. Indeed, not all program variables play the same role in program termination. Some variables are *untrusted*: their values may be externally controlled, for instance by user input, an operating system scheduler, or a third-party library. If controlling such variables alone is sufficient to enforce divergence, we say that the program is vulnerable to *Robust Non-Termination*, which represents a serious concern in practice. By contrast, other variables are *trusted*: their values stem from non-deterministic choices, internal computations, or library calls under the control of the programmer. Non-termination that may be avoided through these trusted choices may be acceptable, as it cannot be reliably exploited by an adversary; it reflects internal system behavior rather than external influence. From a security perspective, this distinction is crucial: divergence caused by untrusted inputs constitutes a potential denial-of-service vulnerability, whereas divergence caused by trusted variables does not. From a software engineering standpoint, the distinction is equally important as it hints at a principled way to triage non-termination alarms, helping developers prioritize the more critical cases.

This distinction motivates the property of *Termination Resilience*; for every possible (sequence of) untrusted input(s), there exists at least one terminating execution. In semantic terms, we treat untrusted variables demonically, since termination must be ensured under all value possibilities, while trusted variables
¹x := input;
²z := 10;
if ³(...) {
    while ⁴(z >= 0) {
        z := z - x;
    }
} else {
    ⁶c := [-2, 1];
    while ⁷(z >= x) {
        z := z + c;
    }
}⁹

<caption>Fig. 1: Program *P*.</caption>

are treated angelically, since it suffices that some of their values enable termina-
tion. Besides, we support both scenarios where untrusted inputs have full and
partial knowledge on trusted variables. Consider program *P* (inspired from our
benchmarks and written in the small programming language that we use for
illustration in the paper) in Figure 1: the variable *x* is an untrusted input (cf.
program label 1), while the value of *c* is non-deterministically chosen between
-2 and 1 (cf. label 6). Both *while* loops in the program are non-terminating,
the first when *x* ≤ 0, and the second when (*z* ≥ *x* and) *c* ≥ 0. However, only for
the first loop (non-)termination depends on untrusted variables, while the sec-
ond loop satisfies Termination Resilience. Termination Resilience thus provides
a nuanced alternative to Termination. Note that in this program the untrusted
input is the first to choose a value (cf. label 1), hence it has no knowledge about
the trusted variables (*c* and *z*) values.

We design an abstract interpretation-based static analysis framework to prove Termination Resilience. Our framework is a generalization of Cousot and Cousot's idea of computing a ranking function by abstract interpretation [12]. Specifically, we extend their semantic definitions to accommodate the asymmetric treatment of untrusted and trusted program variables. We derive a sound static analysis for Termination Resilience by building upon Urban and Miné's decision tree abstract domain [34], enhancing it with novel and non-trivial transformer operators to effectively manage this mixed settings. When unable to prove that a program always satisfies Termination Resilience, our static analysis automatically infers sufficient preconditions that ensure Termination Resilience. For example, for program *P* in Figure 1, our analysis proves Termination Resilience for the second loop and automatically infers the precondition *x* > 0 for the first loop.

Our analysis is implemented in an open-source tool, as an extension of the FUNCTION static analyzer [32], and evaluated on benchmarks drawn from the International Competition on Software Verification (SV-COMP) and modeled after real-world software. The experimental results demonstrate the practical usefulness of the analysis as a means to triage non-termination alarms based on
whether they depend on untrusted or trusted variables, provings developers with
a systematic way to prioritize the most critical cases.

## 2 Termination Resilience

In this section, we give a mathematical characterization of the behavior of a program, and we formally define our property of interest, *Termination Resilience*.

**Program Semantics.** We model the operational behavior of a program as a transition system $\langle\Sigma, \tau\rangle$ where $\Sigma$ is a (potentially infinite) set of program states, and the transition relation $\tau \subseteq \Sigma \times \Sigma$ describes possible transition between states [10,9]. Specifically, for our purposes, $\tau \stackrel{\text{def}}{=} \tau^i \uplus \tau^r$ is the disjoint union of input transitions in $\tau^i$, which are transitions that consume an untrusted input, and regular transitions in $\tau^r$. For simplicity, without loss of generalization, we assume that all transitions $\langle s, s' \rangle \in \tau$ from a state $s \in \Sigma$ are of the same kind, i.e., either all input transition or all regular transitions. The set of final program states is $\Omega_{\tau} \stackrel{\text{def}}{=} \{s \in \Sigma \mid \forall s' \in \Sigma : \langle s, s' \rangle \notin \tau\}$.

Given a transition system $\langle\Sigma, \tau\rangle$, the function $\text{pre}_{\tau^r}: \mathcal{P}(\Sigma) \to \mathcal{P}(\Sigma)$ maps a given set of states $X \subseteq \Sigma$ to the set of their predecessors with respect to $\tau^r$: $\text{pre}_{\tau^r}(X) \stackrel{\text{def}}{=} \{s \in \Sigma \mid \exists s' \in X : \langle s, s' \rangle \in \tau^r\}$, and the function $\tilde{\text{pre}}_{\tau^i}: \mathcal{P}(\Sigma) \to \mathcal{P}(\Sigma)$ maps a set of states $X \subseteq \Sigma$ to the set of states whose successors with respect to $\tau^i$ are all in $X$: $\tilde{\text{pre}}_{\tau^i}(X) \stackrel{\text{def}}{=} \{s \in \Sigma \mid \forall s' \in \Sigma : \langle s, s' \rangle \in \tau^i \Rightarrow s' \in X\}$.

In the following, given a set $S$, let $\varepsilon$ be an empty sequence of elements in $S$, $S^+$ be the set of all non-empty finite sequences of elements in $S$, $S^\omega$ be the set of all infinite sequences, $S^{+\infty} \stackrel{\text{def}}{=} S^+ \cup S^\omega$ be the set of all non-empty finite or infinite sequences of elements in $S$, and $S^{*\infty} \stackrel{\text{def}}{=} S^{+\infty} \cup \{\varepsilon\}$. We write $T^+ \stackrel{\text{def}}{=} T \cap S^+$, $T^\omega \stackrel{\text{def}}{=} T \cap S^\omega$ for the selection of the non-empty finite sequences and the infinite sequences of $T \in \mathcal{P}(S^{+\infty})$, and $T; T' = \{\text{tst}^i \in S^{+\infty} \mid s \in S \wedge \text{ts}^i \in T \wedge \text{st}^i \in T'\}$ for the merging of two sets of sequences $T \in \mathcal{P}(S^+)$ and $T' \in \mathcal{P}(S^{+\infty})$, when a finite sequence in $T$ terminates with the initial element of a sequence in $T'$.

A trace $\sigma \in \Sigma^{+\infty}$ is a non-empty sequence of program states where each pair of consecutive states $s, s' \in \Sigma$ is described by the transition relation $\tau$, i.e., $\langle s, s' \rangle \in \tau$. We write $\sigma_n$ to denote the n-th state of a trace $\sigma \in \Sigma^{+\infty}$ (with $n < |\sigma|$), $\sigma^i$ (resp. $\sigma^r$) for the (possibly empty) sequence of input (resp. regular) transitions (i.e., pairs of consecutive states) in $\sigma$, and $T^i$ for the set $\{\sigma^i \mid \sigma \in T\}$ of sequences of input transitions in traces in a set $T \in \mathcal{P}(\Sigma^{+\infty})$ (resp. $T^r$ for the set $\{\sigma^r \mid \sigma \in T\}$ of sequences of regular transitions). The trace semantics $\Lambda \in \mathcal{P}(\Sigma^{+\infty})$ generated by a transition system $\langle\Sigma, \tau\rangle$ is the union of all non-empty finite traces terminating in $\Omega_{\tau}$, and all infinite traces. It can be expressed as a least fixpoint in the complete lattice $\langle\mathcal{P}(\Sigma^{+\infty}), \sqsubseteq, \sqcup, \sqcap, \Sigma^\omega, \Sigma^+\rangle[9]$:

$$ 
\begin{aligned}
\Lambda &= \text{lfp} \sqsubseteq \Theta \\
\Theta(T) &= \text{def} \Omega_{\tau} \cup (\tau; T)
\end{aligned} 
\qquad (1) $$
<figure><img src="image_4.png" /><figcaption>(a) The transition system $\langle \Sigma_1, \tau_1 \rangle$.</figcaption></figure>

<caption>(b) The transition system $\langle \Sigma_2, \tau_2 \rangle$.</caption>

<caption>Fig. 2: The transition systems of Examples 1 and 2. Input transitions are represented with dashed red lines, while solid black lines represent regular transitions.</caption>

where the computational order is $T_1 \sqsubseteq T_2 \stackrel{\text{def}}{\Rightarrow} T_1^+ \subseteq T_2^+ \wedge T_1^\omega \supseteq T_2^\omega$. In the following, we write $\Lambda[\mathcal{P}]$ to denote the trace semantics of a given program $\mathcal{P}$. Given an initial set of states $I \subseteq \Sigma$, we define $\Lambda[\mathcal{P}]I \stackrel{\text{def}}{=} \{\sigma \in \Lambda[\mathcal{P}] | \sigma_0 \in I\}$ as the restriction of the trace semantics of $\mathcal{P}$ to traces starting in $I$.

**Example 1.** Let $\langle \Sigma_1, \tau_1 \rangle$ be a transition system with $\Sigma_1 = \{a, b, c\}$ and $\tau_1 = \tau_1^i \cup \tau_1^r$ where $\tau_1^i = \{\langle a, b \rangle, \langle a, c \rangle\}$ and $\tau_1^r = \{\langle c, c \rangle\}$ (cf. Figure 2a). The trace semantics generated by $\langle \Sigma_1, \tau_1 \rangle$ and starting in $I = \{a\}$ is $\Lambda_1 = \{ab, ac^\omega\}$. $\triangleleft$

**Example 2.** Let $\langle \Sigma_1, \tau_1 \rangle$ be the transition system from Example 1 and let $\langle \Sigma_2, \tau_2 \rangle$ be another transition system with $\Sigma_2 = \Sigma_1 \cup \{d, e\}$ and $\tau_2 = \tau_1^i \cup \tau_2^r$ where $\tau_2^r = \tau_1^r \setminus \{\langle c, c \rangle\} \cup \{\langle b, d \rangle, \langle b, e \rangle, \langle e, e \rangle\}$ (cf. Figure 2b). The trace semantics generated by $\langle \Sigma_2, \tau_2 \rangle$ and starting in $I = \{a\}$ is $\Lambda_2 = \{abd, abe^\omega, ac\}$. $\triangleleft$

**Program Property.** As customary in abstract interpretation [10], we represent properties of entities in a universe $\mathbb{U}$ by a subset of this universe. We formally define the Robust Non-Termination program property.

**Definition 1 (Robust Non-Termination).** The Robust Non-Termination program property is the set of sets of traces for which a (possibly empty) sequence of input transitions only yields diverging traces:

$$ \mathcal{RT} \stackrel{\text{def}}{=} \{ T \in \mathcal{P}(\Sigma^{+\infty}) \mid \exists j \in T^i \ \forall \sigma \in T: \sigma^i = j \Rightarrow \sigma \in T^\omega \} \quad (2) $$

Note that any set $T \subseteq \mathcal{P}(\Sigma^\omega)$ of infinite traces always belongs to $\mathcal{RT}$, even if the traces do not consume input values (in such case $j = \varepsilon$), i.e., an always non-terminating program is always vulnerable to non-termination exploits.

**Example 3.** Let $\langle \Sigma_1, \tau_1 \rangle$ be the transition system from Example 1. The input transition $\langle a, c \rangle$ only yields the diverging trace $ac^\omega \in \Lambda_1$. Thus $\Lambda_1 \in \mathcal{RT}$. $\triangleleft$

The negation of Robust Non-Termination is our property of interest. It expresses the ability of the program to (possibly) defend itself from non-termination exploits. Formally, we call this property *Termination Resilience*.
**Definition 2 (Termination Resilience).** The Termination Resilience program property is the set of sets of program traces for which there exists a terminating trace for all sequence of input transitions:

$$ \mathcal{TR} \stackrel{\text{def}}{=} \neg \mathcal{RNT} = \{T \in \mathcal{P}(\Sigma^{+\infty}) \mid \forall j \in T^i \exists \sigma \in T^+: \sigma^i = j\} \quad (3) $$

*Example 4.* Let $\langle \Sigma_2, \tau_2 \rangle$ be the transition system from Example 2. For any sequence of input transitions in $(\Lambda_2)^i = \{\langle a, b \rangle, \langle a, c \rangle\}$, there is at least one terminating trace in $\Lambda_2$, i.e., abd for $\langle a, b \rangle$, and ac for $\langle a, c \rangle$. Thus, $\Lambda_2 \in \mathcal{TR}$. $\triangleleft$

The trace semantics $\Lambda[[P]]$ of a program $P$, fully describing the behavior of $P$, exactly characterizes Termination Resilience of $P$ (and its negation, Robust Non-Termination), for an initial set of states $I \subseteq \Sigma$:

$$ P \models_I \mathcal{TR} \Leftrightarrow \Lambda[[P]]I \in \mathcal{TR} \Leftrightarrow \Lambda[[P]]I \notin \mathcal{RNT} \Leftrightarrow P \not\models_I \mathcal{RNT}. \quad (4) $$

In the next two sections, we abstract the trace semantics $\Lambda$ to a special-purpose sound and complete (but not computable) semantics $\Lambda_{\text{tr}}$ that forgets details of the program behavior that are irrelevant for reasoning about Termination Resilience. Next, we further abstract this semantics into a sound but computable semantics $\Lambda_{\text{tr}}^\flat$ that yields a static analysis for Termination Resilience.

## 3 Termination Resilience Semantics

We derive our concrete semantics $\Lambda_{\text{tr}}$ by abstract interpretation of the trace semantics $\Lambda$. The abstraction eliminates program traces that are potentially branching to non-termination through different untrusted inputs, and proves Termination Resilience for the remaining traces by associating a well-founded quantity [31,13] to program states belonging to terminating traces. Specifically, we abstract the trace semantics $\Lambda \in \mathcal{P}(\Sigma^{+\infty})$ into the termination resilience semantics $\Lambda_{\text{tr}}: \Sigma \to \mathcal{O}$ (where $\mathcal{O}$ is the set of ordinals), which is the best (potential) ranking function [12,33] for the program states in the traces in $\Lambda$.

We define the termination resilience abstraction $\alpha_{\text{tr}}: \mathcal{P}(\Sigma^{+\infty}) \to (\Sigma \to \mathcal{O})$ to map sets of program traces to a (potential) ranking function as:

$$ \alpha_{\text{tr}}(T) \stackrel{\text{def}}{=} \alpha_v \circ \overrightarrow{\alpha}(T) \quad (5) $$

where $\overrightarrow{\alpha}: \mathcal{P}(\Sigma^{+\infty}) \to \mathcal{P}(\Sigma \times \Sigma)$ extracts the smallest transition relation $\tau \subseteq \Sigma \times \Sigma$ that generates a given set of traces $T: \overrightarrow{\alpha}(T) \stackrel{\text{def}}{=} \{\langle s, s' \rangle \mid \exists \sigma, \sigma': \sigma s s' \sigma' \in T\}$, and $\alpha_v: \mathcal{P}(\Sigma \times \Sigma) \to (\Sigma \to \mathcal{O})$ ranks the elements in the domain of $r$:

$$ \alpha_v(\emptyset) \stackrel{\text{def}}{=} \emptyset \\ \alpha_v(r)s \stackrel{\text{def}}{=} \left\{ \begin{array}{ll} 0 & s \in \Omega_r \\ \sup \left\{ \alpha_v(r)s' + 1 \middle| \langle s, s' \rangle \in r^i \right\} & s \in \widetilde{\text{pre}}_{r^i}(\text{dom}(\alpha_v(r))) \\ \inf \left\{ \alpha_v(r)s' + 1 \middle| \text{dom}(\alpha_v(r)) \wedge \langle s, s' \rangle \in r^r \right\} & s \in \text{pre}_{r^r}(\text{dom}(\alpha_v(r))) \\ \text{undefined} & \text{otherwise} \end{array} \right. $$
with $\emptyset$ representing the totally undefined function. The (potential) ranking function is defined incrementally, starting from the final states in $\Omega_r$, where the function has value 0 (and is undefined elsewhere). Then, the domain of the function grows by retracing the program (transitions) backwards and counting the number of performed program steps as value of the function. We model the non-determinism arising from input transitions *demonically*, requiring all successor states to already be in the domain of the function ($s \in \tilde{\mathrm{pre}}_{r^i}(\mathrm{dom}(\alpha_v(r)))$), and count the *maximum* number of performed program steps. Instead, non-determinism arising from regular transitions is treated *angelically*, and the potential ranking functions counts the minimum number of steps to termination.

We can now formally define the termination resilience semantics $\Lambda_{\mathrm{tr}}$.

**Definition 3 (Termination Resilience Semantics).** Let $\langle\Sigma, \tau\rangle$ be a transition system. Its termination resilience semantics $\Lambda_{\mathrm{tr}} \in (\Sigma \to \mathbb{O})$ is:

$$ \Lambda_{\mathrm{tr}} \stackrel{\mathrm{def}}{=} \alpha_{\mathrm{tr}}(\Lambda) = \mathrm{lfp} \frac{\Box}{\emptyset} \Theta_{\mathrm{tr}} \\ \Theta_{\mathrm{tr}}(f) \stackrel{\mathrm{def}}{=} \lambda s. \left\{ \begin{array}{ll} 0 & s \in \Omega_{\tau} \\ \sup \{f(s') + 1 \mid \langle s, s' \rangle \in \tau^i\} & s \in \tilde{\mathrm{pre}}_{\tau^i}(\mathrm{dom}(f)) \\ \inf \{f(s') + 1 \mid s' \in \mathrm{dom}(f), \langle s, s' \rangle \in \tau^r\} & s \in \mathrm{pre}_{\tau^r}(\mathrm{dom}(f)) \\ \mathrm{undefined} & \text{otherwise} \end{array} \right. $$

where $\Lambda \in \mathcal{P}(\Sigma^{+\infty})$ is the trace semantics (cf. Equation 2).

We write $\Lambda_{\mathrm{tr}}[P]$ for the termination resilience semantics of a program $P$.

**Example 5.** Let $\langle\Sigma_2, \tau_2\rangle$ and $\Lambda_{t2}$ be the transition system from Example 2 and its termination resilience trace semantics, respectively. The fixpoint iterates of its termination resilience semantics $\Lambda_{\mathrm{tr}2} \stackrel{\mathrm{def}}{=} \alpha_{\mathrm{tr}}(\Lambda_{t2})$ are the following:

<figure><img src="image_5.png" /></figure>

Note that $\Lambda_{\mathrm{tr}2}$ is defined over the state $b$ even if a transition can lead to the diverging trace $be^\omega$ because the non-deterministic choice is treated angelically: there is at least one choice that ensures termination (via the trace $bd$). $\triangleleft$

The termination resilience semantics $\Lambda_{\mathrm{tr}}[P]$ of a program $P$ is sound and complete for verifying Termination Resilience, for an initial set of states $I \subseteq \Sigma$:

**Theorem 1 (Soundness&Completeness).** $\Lambda[\![P]\!] \in \mathcal{TR} \Leftrightarrow I \subseteq \mathrm{dom}(\Lambda_{\mathrm{tr}}[\![P]\!])$
<figure><img src="image_6.png" /><figcaption>(a) Program $P_1$</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>(b) Program $P_2$</figcaption></figure>

<caption>Fig. 3: Programs akin to the transitions systems in Example 1 (a) and 2 (b).</caption>

# 4 Denotational Termination Resilience Semantics

The formal treatment given in the previous section is language independent. In the following, for simplicity, we introduce a small sequential programming language that we use for illustration throughout the rest of the paper:

$$AExp \ni a ::= x \mid c \mid -a \mid a \diamond a$$

$$ \begin{align*} \text{Stmt} \ni s &::= {}^l \text{skip} \mid {}^l x := \text{input} \mid {}^l x := [c_1, c_2] \mid {}^l x := a \\ &\phantom{::=} \mid \text{if} \, {}^l a \bowtie 0 \{s\} \mid \text{while} \, {}^l a \bowtie 0 \{s\} \mid s; s \end{align*} $$

$$ \text{Prog} \ni p ::= s^l $$

where $x \in \mathcal{X}$ ranges over program variables, $c \in \mathbb{Z}$, $c_1 \in \mathbb{Z} \cup \{-\infty\}$, $c_2 \in \mathbb{Z} \cup \{+\infty\}$ range over mathematical integer values possibly extended to include (negative or positive) infinity, $\diamond \in \{+, -, *, \dots \}$, and $\bowtie \in \{=, \ne, \le, \dots \}$. A unique label $l \in \mathcal{L}$ appears within each instruction statement. Variable assignments can involve an untrusted input ($^{l}x := \text{input}$), a (trusted) non-deterministic choice ($^{l}x := [c_1, c_2]$) or an arithmetic expression ($^{l}x := a$). A program is an instruction statement $s \in \text{Stmt}$ followed by a label $l \in \mathcal{L}$.

Figure 3 shows two programs written in our small language, both slices of program *P* from Figure 1. Program $P_1$ (cf. Figure 3a) is akin to the transition system in Example 1: the input $x \le 0$ leads to non-termination (state *c* in Figure 2a), while for $x > 0$ (state *b*) the program always terminates. Instead, $P_2$ (cf. Figure 3b) is akin to Example 2: for the input $x \le 10$ (state *b* in Figure 2b), termination is possible with $c < 0$ (state *d*).

In this section, we instantiate the definition of our termination resilience semantics $\Lambda_{\text{tr}}$ with respect to programs $p \in \text{Prog}$ written in our small language. Then, in the next section, we will define its abstraction $\Lambda_{\text{tr}}^b$.

**Taint Semantics.** Let $\mathcal{E} = \mathcal{X} \to \mathbb{Z}$ denote the set of environments, where each $\rho \in \mathcal{E}$ maps variables to their integer values. We adopt the standard semantics of expressions $[e] : \mathcal{E} \to \mathcal{P}(\mathbb{Z})$ mapping an expression $e \in AExp \cup \{\text{input}, [c_1, c_2]\}$ to the set of all its possible values in a given environment.

Program states are pairs $\mathcal{L} \times \mathcal{E}$ of a label $l \in \mathcal{L}$ and an environment $\rho \in \mathcal{E}$ defining the values of the program variables at the program point designated
$$
\begin{align*}
\mathfrak{T}^{[l]} \text{skip}] \T T &\stackrel{\text{def}}{=} \T T \\
\mathfrak{T}^{[l]} x := \textcolor{red}{\text{input}] \T T} &\stackrel{\text{def}}{=} \T T \cup \{x\} \\
\mathfrak{T}^{[l]} x := [c_1, c_2]] \T T &\stackrel{\text{def}}{=} \T T \setminus \{x\} \\
\mathfrak{T}^{[l]} x := \mathbf{a}] \T T &\stackrel{\text{def}}{=} \left\{ \begin{array}{ll} \T T \cup \{x\} & \mathfrak{T}[\mathbf{a}] \T T \\ \T T \setminus \{x\} & \text{otherwise} \end{array} \right. \\
\mathfrak{T}^{[\text{if}^l \mathbf{a} \succcurlyeq 0 \{\mathbf{s}\}]} \T T &\stackrel{\text{def}}{=} \left\{ \begin{array}{ll} \mathfrak{T}[\mathbf{s}] \T T \cup \text{ASSIGNED}(\mathbf{s}) \cup \T T & \mathfrak{T}[\mathbf{a}] \T T \\ \mathfrak{T}[\mathbf{s}] \T T \cup \T T & \text{otherwise} \end{array} \right. \\
\mathfrak{T}^{[\text{while}^l \mathbf{a} \succcurlyeq 0 \{\mathbf{s}\}]} \T T &\stackrel{\text{def}}{=} \text{If } \mathbf{p} \subseteq \mathfrak{T}^{[\text{if}^l \mathbf{a} \succcurlyeq 0 \{\mathbf{s}\}]} \\
\mathfrak{T}[\mathbf{s}_1; \mathbf{s}_2] \T T &\stackrel{\text{def}}{=} \mathfrak{T}[\mathbf{s}_2](\mathfrak{T}[\mathbf{s}_1] \T T)
\end{align*}
$$

<caption>Fig. 4: Taint semantics $\mathfrak{T}[\mathbf{s}] : \mathcal{P}(\mathcal{X}) \to \mathcal{P}(\mathcal{X})$, where $\text{ASSIGNED}(\mathbf{s})$ is the set of variables assigned with an arithmetic expression within the statement $\mathbf{s}$.</caption>

by $l$. To track the effect of input transitions on program states, we need a taint semantics $\mathfrak{T}[\mathbf{s}] : \mathcal{P}(\mathcal{X}) \to \mathcal{P}(\mathcal{X})$ that collects variables that depend on untrusted inputs, i.e., that are tainted, after the execution of a program statement (cf. Figure 4). The taint semantics $\mathfrak{T}[\mathbf{a}] : \mathcal{P}(\mathcal{X}) \to \{\text{true, false}\}$ of expressions is:

$$
\mathfrak{T}[\mathbf{a}]\T T \stackrel{\text{def}}{=} \exists \rho \in \mathcal{E} : \exists V \in \mathbb{Z}^{|X|} : V \in [\mathbf{a}]\rho \wedge \forall \rho' \neq_T \rho : V \notin [\mathbf{a}]\rho' \quad (6)
$$

where $\rho' \neq_T \rho \Leftrightarrow \exists \emptyset \subset T' \subseteq T : (\forall x \notin T' : \rho(x) = \rho'(x)) \wedge (\forall x \in T' : \rho(x) \neq \rho'(x))$ denotes program environments that differ only on (a non-empty subset of) the tainted variables in T. An expression is tainted if there exists a value of its semantics $[\mathbf{a}]$ that is only possible in an environment $\rho$ with a certain value $V$ for the set $T$ of tainted variables, i.e., the value of the expression depends on untrusted program inputs. Note that this definition differs from a classical non-interference-like definition (e.g., $\mathfrak{T}[\mathbf{a}]\T T \stackrel{\text{def}}{=} \forall \rho, \rho' \in \mathcal{E} : \forall x \notin T : \rho(x) = \rho'(x) \wedge [\mathbf{a}]\rho \neq [\mathbf{a}]\rho'$) to also take into account the non-determinism arising from trusted variables (i.e., $[\mathbf{a}]\rho \neq [\mathbf{a}]\rho'$ could be the consequence of non-deterministic value choices rather than untrusted inputs). For simplicity, in this definition we deliberately do not take into account the reachable environments at each program label. A more precise definition would be straightforward but needlessly cumbersome for our purposes. The taint semantics $\mathfrak{T}[\mathbf{p}] \in \mathcal{P}(\mathcal{X})$ of a program $\mathbf{p} \in \text{Prog}$ is $\mathfrak{T}[\mathbf{p}] = \mathfrak{T}[\mathbf{s}^l] \stackrel{\text{def}}{=} \mathfrak{T}[\mathbf{s}]\emptyset$. By pointwise-lifting of $\mathfrak{T}$ with respect to the program labels $\mathcal{L}$, we obtain the lifted taint semantics $\tilde{\mathcal{T}} : \mathcal{L} \to \mathcal{P}(\mathcal{X})$ mapping each label to the set of variables that are can be tainted at that label.

**Denotational Termination Resilience Semantics.** We can now define in Figure 5 the termination resilience semantics $\Lambda_{\text{tr}}[\mathbf{s}] : (\mathcal{E} \to \mathcal{O}) \to (\mathcal{E} \to \mathcal{O})$ for
$$ \Lambda_{\text{tr}}[^l \text{skip}]f \stackrel{\text{def}}{=} \lambda\rho \in \text{dom}(f).f(\rho) + 1 $$

$$ \Lambda_{\text{tr}}[^l x := \mathbf{e}]f \stackrel{\text{def}}{=} \lambda\rho. \left\{ \begin{array}{l} \sup\{f(\rho[x \leftarrow v]) + 1 \mid v \in [\mathbf{e}]\rho\} \qquad \mathbf{e} = \text{input} \lor A \\ \inf\left\{f(\rho[x \leftarrow v]) + 1 \mid \begin{array}{l} v \in [\mathbf{e}]\rho \land \\ \rho[x \leftarrow v] \in \text{dom}(f) \end{array}\right\} \qquad \mathbf{e} = [c_1, c_2] \lor B \\ \text{undefined} \qquad \text{otherwise} \end{array} \right. $$

$$ A \Leftrightarrow (\mathbf{e} = \mathbf{a} \land \mathfrak{T}[\mathbf{a}](\dot{\mathfrak{T}}(l)) \land \exists v \in [\mathbf{a}]\rho \land \forall v \in [\mathbf{a}]\rho, \rho[x \leftarrow v] \in \text{dom}(f)) $$

$$ B \Leftrightarrow (\mathbf{e} = \mathbf{a} \land \neg \mathfrak{T}[\mathbf{a}](\dot{\mathfrak{T}}(l)) \land \exists v \in [\mathbf{a}]\rho : \rho[x \leftarrow v] \in \text{dom}(f)) $$

$$ \Lambda_{\text{tr}}[\text{if}^l \mathbf{a} \triangleright 0 \{\mathbf{s}\}]f \stackrel{\text{def}}{=} \Theta_{\text{tr}}(f) $$

$$ \Theta_{\text{tr}} \stackrel{\text{def}}{=} \lambda X. \lambda \rho. \left\{ \begin{array}{ll} \Lambda_{\text{tr}}[\mathbf{s}]X(\rho) + 1 & \forall v \in [\mathbf{a}]\rho : v \triangleright 0 \land \rho \in \text{dom}(\Lambda_{\text{tr}}[\mathbf{s}]X(\rho)) \\ f(\rho) + 1 & \forall v \in [\mathbf{a}]\rho : v \triangleright 0 \land \rho \in \text{dom}(f(\rho)) \\ \text{undefined} & \text{otherwise} \end{array} \right. $$

$$ \Lambda_{\text{tr}}[\text{while}^l \mathbf{a} \triangleright 0 \{\mathbf{s}\}]f \stackrel{\text{def}}{=} \text{lfp}_{\emptyset}^{\subseteq} \Theta_{\text{tr}} $$

$$ \Lambda_{\text{tr}}[\mathbf{s}_1; \mathbf{s}_2]f \stackrel{\text{def}}{=} \Lambda_{\text{tr}}[\mathbf{s}_1](\Lambda_{\text{tr}}[\mathbf{s}_2]f) $$

<caption>Fig. 5: Termination resilience semantics $\Lambda_{\text{tr}}[\mathbf{s}] : (\mathcal{E} \to \mathcal{O}) \to (\mathcal{E} \to \mathcal{O})$. Since $[\mathbf{a}]\rho$ is always a singleton $\{v\}$, we abuse notation and write $[\mathbf{a}]\rho$ to directly denote $v$.</caption>

each program statement. Each transfer function $\Lambda_{\text{tr}}[\mathbf{s}]$ takes as input a (potential) ranking function that is valid *after* the execution of the statement $\mathbf{s}$ and returns a (potential) ranking function that is valid *before* the execution of $\mathbf{s}$.

If the right-hand side of an assignment is an untrusted input ($^l x := \text{input}$) or an expression $\mathbf{a}$ ($^l x := \mathbf{a}$) that depends on tainted variables ($\mathfrak{T}[\mathbf{a}]$(\dot{\mathfrak{T}}(l)))}, the termination resilience semantics $\Lambda_{\text{tr}}[^l x := \mathbf{a}]$ returns a (potential) ranking function only defined over the environments $\rho$ that, when subject to the assignment ($\rho[x \leftarrow v]$ with $v \in [\mathbf{a}]\rho$), always belong to the domain of the given (potential) ranking function $f$ (case A). The value of $f$ for these environments is increased by one, to take into account another program execution step before termination, and the value of the resulting ranking function is the least upper bound of these values (to count the maximum number of steps to termination). Otherwise – if the right-hand side of the assignment is a non-deterministic choice ($^l x := [c_1, c_2]$) or an expression $\mathbf{a}$ that does not depend on tainted variables ($\neg \mathfrak{T}[\mathbf{a}]$(\dot{\mathfrak{T}}(l))) – the resulting function is defined over the environments $\rho$ for which *at least one* value $v \in [\mathbf{a}]\rho$ yields an environment $\rho[x \leftarrow v]$ in $\text{dom}(f)$ (case B). Its value is the greatest lower bound of the value of $f$ on these environments plus one (to count the minimum number of steps to termination).

The termination resilience semantics $\Lambda_{\text{tr}}[\text{if}^l \mathbf{a} \triangleright 0 \{\mathbf{s}\}]$ for *if* statements, via $\Theta_{\text{tr}}$, defines a potential ranking function over all environments in $\text{dom}(\Lambda_{\text{tr}}[\mathbf{s}]f)$ or $\text{dom}(f)$, i.e., all environments potentially leading to a terminating execution, depending on whether they satisfy or not satisfy the guard $\mathbf{a} \triangleright 0$. The termination
resilience $\Lambda_{\text{tr}}[\text{while}^l \text{a} \triangleright 0 \{\mathbf{s}\}]$ for while statements is the least fixpoint of $\Theta_{\text{tr}}$ with respect to the computational order $f_1 \subseteq f_2 \stackrel{\text{def}}{\rightleftharpoons} \text{dom}(f_1) \subseteq \text{dom}(f_2) \wedge \forall x \in \text{dom}(f_1): f_1(x) \le f_2(x)$.

The termination resilience semantics $\Lambda_{\text{tr}}[\mathbf{p}] \in (\mathcal{E} \to \mathcal{O})$ of a program $\mathbf{p} \in \text{Prog}$ is determined by $\Lambda_{\text{tr}}[\mathbf{s}]$ taking as input the constant function equal to zero.

**Definition 4 (Denotational Termination Resilience Semantics).** Let $\mathbf{p} \in \text{Prog}$ be a program. Its denotational termination resilience semantics is:

$$ \Lambda_{\text{tr}}[\mathbf{p}] = \Lambda_{\text{tr}}[\mathbf{s}^l] \stackrel{\text{def}}{=} \Lambda_{\text{tr}}[\mathbf{s}](\lambda\rho.0). \qquad (7) $$

# 5 Abstract Termination Resilience Semantics

In this section, we propose a sound abstraction $\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}]$ of the denotational termination resilience semantics $\Lambda_{\text{tr}}[\mathbf{p}]$ defined in Section 4 by leveraging (and extending) Urban and Miné's decision tree numerical abstract domain $\mathcal{T}$ [34] to abstract potential ranking functions by means of piecewise-defined partial functions. Specifically, we consider the concretization-based abstraction $[11] \langle \mathcal{E} \to \mathcal{O}, \preceq \rangle \leftarrow \gamma \langle \mathcal{T}, \preceq_T \rangle$ where the approximation order $\preceq$ is defined as follows:

$$ f_1 \preceq f_2 \Leftrightarrow \text{dom}(f_1) \supseteq \text{dom}(f_2) \wedge \forall x \in \text{dom}(f_2): f_1(x) \le f_2(x). \qquad (8) $$

We define $\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}]$ so $\Lambda_{\text{tr}}[\mathbf{p}] \preceq \gamma(\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}])$ meaning that $\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}]$ over-approximates the value of $\Lambda_{\text{tr}}[\mathbf{p}]$ and under-approximates its domain $\text{dom}(\Lambda_{\text{tr}}[\mathbf{p}])$. In this way, the abstraction $\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}]$ provides sufficient preconditions for termination resilience.

**Remark 1.** Note that Urban and Miné's abstract termination semantics [34] — let us denote it $\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}]$ — is already a sound but coarse over-approximation of $\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}]$: $\Lambda_{\text{tr}}[\mathbf{P}] \preceq \gamma(\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}])$. Our objective in this section is to build upon and relax $\Lambda_{\text{tr}}^{\mathfrak{t}}[\mathbf{p}]$ for reasoning about Termination Resilience.

## 5.1 Decision Tree Abstract Domain.

In the following, we recall the decision tree abstract domain only insofar as it is necessary for our analysis. We do not redefine aspects of the domain that remain unchanged, and refer to [33] for the full formal definitions.

An element $t \in \mathcal{T}$ is a piecewise-defined partial function represented by a full binary tree, where each node — denoted $\text{NODE}\{c\}$: $t_1, t_2$, with $t_1, t_2 \in \mathcal{T}$ — is labeled by a constraint $c \in \mathcal{C}$ over the program variables (where $\mathcal{C}$ is the set of allowed constraints, e.g., linear constraints), and each leaf — denoted $\text{LEAF}$: $f$ — is labeled by a function $f \in \mathcal{F}$ of the program variables (where $\mathcal{F}$ is the set of allowed functions, e.g., affine functions). Nodes recursively partition the space of possible values of the program variables: constraint labeling nodes are satisfied by the left subtrees of the nodes, while the right subtrees satisfy their negation. The leaves of the tree represent the value of the function within each partition.
<table><caption>**Algorithm 1 Decision Tree Assignment**</caption><tr><td>1:</td><td>function ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>(t)</td></tr><tr><td>2:</td><td>if isLeaf(t) then</td></tr><tr><td>3:</td><td>return LEAF: ASSIGN<sub>F</sub>[<sup>l</sup><sub>x := e</sub>(t.f)</td></tr><tr><td>4:</td><td>else if isNode(t) then</td></tr><tr><td>5:</td><td>I &larr; ASSIGN<sub>C</sub>[<sup>l</sup><sub>x := e</sub>(t.c)</td></tr><tr><td>6:</td><td>J &larr; ASSIGN<sub>C</sub>[<sup>l</sup><sub>x := e</sub>(&not;t.c)</td></tr><tr><td>7:</td><td>if empty(I) &amp; empty(J) then</td></tr><tr><td>8:</td><td>return ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>(t.l) &amp; T ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>(t.r)</td></tr><tr><td>9:</td><td>else if empty(I) &amp; &perp;<sub>C</sub> &isin; J then</td></tr><tr><td>10:</td><td>return ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>(t.l)</td></tr><tr><td>11:</td><td>else if &perp;<sub>C</sub> &isin; I &amp; empty(J) then</td></tr><tr><td>12:</td><td>return ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>(t.r)</td></tr><tr><td>13:</td><td>else</td></tr><tr><td>14:</td><td>t<sub>1</sub> &larr; PRUNE<sub>T</sub>(ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>(t.l), I)</td></tr><tr><td>15:</td><td>t<sub>2</sub> &larr; PRUNE<sub>T</sub>(ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>(t.r), J)</td></tr><tr><td>16:</td><td>return t<sub>1</sub> &amp; T t<sub>2</sub></td></tr></table>

Figure 6 shows an example of a decision tree. The leaf with value $\perp_F$ explicitly represents the undefined partition of the (partial) function. Undefined functions can also be represented by the leaf value $\top_F$ in case of an irrecoverable loss of precision of the analysis [8]. The decision tree in Figure 6 is automatically inferred by our termination resilience static analysis at label 4 of program $P_2$ in Figure 3b. It represents a function with constant value 1

<figure><img src="image_8.png" /><figcaption>Fig. 6: Decision tree inferred by our analysis at label 4 of program $P_2$ (cf. Figure 3b).</figcaption></figure>

when $z < x$ (at most one step to termination), with constant value 3 when $z \ge x \land z + c < x$ (at most three steps to termination) and undefined otherwise (termination is not proved when $z + c \ge x$), while the concrete termination resilience semantics at the same label 4 is defined when $z < x$ or $c < 0$: the decision tree is thus a sound approximation with respect to $\leq$ (cf. Equation 8).

The partitioning induced by decision tree constraints is dynamic: the analysis begins at the end of the program with the decision tree LEAF: 0 (i.e., zero program executions steps to termination) and proceeds backwards; during the analysis, constraints are added by boolean conditions or when merging control flows, and are modified by variable assignments.

Algorithm 1 shows the decision tree assignment operator ASSIGN<sub>T</sub>[<sup>l</sup><sub>x := e</sub>] originally defined in [33]. The assignment is performed by recursively descending the given decision tree t (cf. Lines 14 and 15, the left subtree is accessed with t.l and the right one with t.r). At the leaves, the assignment is handled by the auxiliary operator ASSIGN<sub>F</sub>[<sup>l</sup><sub>x := e</sub>] operating on functions (accessed by t.f, cf. Line 3): after the assignment, the value of defined functions is increased by one to account for one more step to termination. For example, let us consider the
<figure><img src="image_9.png" /><figcaption>(a) Approximation order</figcaption></figure>

$\leq_F$

<caption>(b) Computational order</caption>

$\sqsubseteq_F$

<caption>(c) Resilience order
$\leq_F$</caption>

<caption>Fig. 7: Hasse diagrams for difference orders of decision tree leaves.</caption>

decision tree in Figure 6 and the assignment $c := [-2, 1]$ at label 3 in Figure 3b. The result of the assignment on LEAF : 3 is LEAF : 4, simply increasing the value of its function by one, while LEAF : $\perp_F$ remains unchanged. Node constraints (accessed with t.c) and their negation ($\neg t.c$) are handled by the standard assignment operator $\text{ASSIGN}_C[[x := e]]$ of an auxiliary underlying numerical abstract domain used to manage constraints in $C$, which produces a set $I \in \mathcal{P}(C)$ (cf. Line 5) and a set $J \in \mathcal{P}(C)$ (cf. Line 6) of linear constraint conjuncts resulting from (over-approximating) the assignment to t.c and $\neg t.c$, respectively. For example, considering again the decision tree in Figure 6, the result of the assignment $c := [-2, 1]$ on the constraint $z + c - x \ge 0$ and its negation $z + c - x < 0$ yields $I = \{z - x \ge -1\}$ and $J = \{z - x < 2\}$. The set of constraints $I$ and $J$ are added (by PRUNE$_T$) to the subtrees resulting from the recursive calls (cf. Lines 14 and 15). In our example, the pruning of the LEAF : $\perp_F$ with the set of constraints $I$ results in the decision tree shown in Figure 8a, while the pruning of LEAF : 4 with $J$ results in the tree in Figure. 8b.

<figure><img src="image_10.png" /><figcaption>(a) Pruning of LEAF: $\perp_F$
with $I = \{z - x \ge -1\}$.</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>(b) Pruning of LEAF: 4
with $J = \{z - x < 2\}$.</figcaption></figure>

<caption>Fig. 8: Decision trees resulting from PRUNE$_T$.</caption>

The special NIL node denotes partitions that are outside the domain of definition of the decision tree. Note that it differs from leaves labeled with $\perp_F$ or $\top_F$, which denote undefined partitions within the domain of definition of the tree. Finally, the resulting trees are joined by the approximation join $\gamma_T$ (cf. Line 16), which merges the domains of definitions of the joined trees (essentially removing any NIL nodes) and retains the leaves labeled with an undefined function ($\perp_F$ or $\top_F$) in either of the joined decision trees, cf. the Hasse diagram in Figure 7a. Continuing the example, joining the trees in Figure 8 yields the tree in Figure 9.

<figure><img src="image_12.png" /><figcaption>Fig. 9: Approximation join of Figure 8a and Figure 8b.</figcaption></figure>
<figure><img src="image_13.png" /><figcaption>Fig. 10: Resilience join of Figure 8a and Figure 8b.</figcaption></figure>

In case both *I* and *J* are empty (cf. Line 7), neither the constraint *t.c* nor its negation *¬t.c* exists anymore and thus the subtrees resulting from the recursive calls are joined by the approximation join $\gamma_T$. In case *I* is empty and *J* is an unsatisfiable set of constraints (i.e., the unsatisfiable constraint $\perp_C$ belongs to *J*, cf. Line 9), it means that *¬t.c* is no longer satisfiable and thus only the left subtree of the decision tree is kept (cf. Line 10). Similarly, in case *I* is an unsatisfiable set of constraints and *J* is empty (cf. Line 11), only the right subtree of the decision tree is kept (cf. Line 12).

To minimize the cost of the analysis and to enforce its termination, a widening operator $\nabla_T$ limits the height of the decision trees and the number of induced partitions. Abstract fixpoint iterations with widening follow the computational order $\sqsubseteq_T$, which preserves decision tree leaves labeled with a defined function over undefined leaves labeled with $\perp_F$ (i.e., the analysis grows the domain of the inferred ranking function at each iteration), but preserves leaves labeled with $\top_F$ over all other leaves (i.e., the domain of the inferred function shrinks when the analysis loses too much precision), cf. Figure 7b.

## 5.2 Non-Deterministic Assignments.

To leverage the decision tree abstract domain for termination resilience we need to extend it to distinguish between variables assigned with untrusted or (trusted) non-deterministic values. Termination must be ensured for *all* possible values of untrusted variables, while *any* non-deterministic value that ensures termination is enough to satisfy termination resilience. We thus introduce a new *resilience join* operator $\vee_T$ between decision trees that retains the leaves labeled with a *defined* function in either of the joined decision trees, cf. Figure 7c.

We implement $ASSIGN_T[\llbracket l \ x \ :=[c_1, c_2]\rrbracket]$ for non-deterministic assignments following Algorithm 1, but using the resilience join $\vee_T$ instead of the approximation join $\gamma_T$ at Lines 8 and 16. Let us consider again the left subtree in Figure 6 and the non-deterministic variable assignment $c := [-2, 1]$ at label 3 in Figure 3b. Joining the trees in Figure 8 resulting from the $PRUNE_T$ at Lines 14 and 15 yields the decision tree in Figure 10, which indicates that the termination of program $P_2$ is possible when $z - x < 2$, for at least some values of $c$ chosen at label 3 (notably,

<figure><img src="image_14.png" /><figcaption>Fig. 11: Decision tree inferred at label 3 of program $P_2$.</figcaption></figure>
for $c \in \{-2, -1\}$, but the analysis does not explicitly provide these values). The
final decision tree at program label 3 is shown in Figure 11.

Note that this seemingly anodyne modification is actually insidious. Let us consider
the decision tree in Figure 12 and the variable assignment $x := [-\infty, +\infty]$, and assume that
the variable $y$ is untrusted. The result of the
assignment on the decision tree constraints is
the empty set of constraints and, since the
variable $x$ is assigned with a non-deterministic
value, we can employ the resilience join $\underline{\vee}_F$
to join all leaves after the assignment is performed on them. This yields the final decision tree LEAF: 2 (obtained from
LEAF: 1 after the assignment), which is not sound! In fact, the sufficient pre-
condition for Termination Resilience given by the decision tree in Figure 12
requires $y > 0$ but this constraint is missing from the decision tree because it is
redundant. As a consequence, when the assignment is performed and the other
constraints $x < 0$ and $x + y \ge 0$ disappear, the result is an unsound decision
tree indicating that termination resilience always holds. To avoid this issue, be-
fore non-deterministic variable assignments, decision trees need to be filled to
explicitly contain at least the strongest redundant univariate constraints over
the untrusted program variables. We further modify Algorithm 1 to insert a call
to FILL$_T(t)$ at the very beginning (before Line 2), where FILL$_T$ leverages the un-
derlying numerical abstract domain used to manage $C$ to find these redundant
univariate constraints and adds them to the decision tree $t$. Additional redundant
constraints may be added, though this needlessly increases the analysis time.

<figure><img src="image_15.png" /><figcaption>Fig. 12: Unfilled decision tree.</figcaption></figure>

The ASSIGN$_T$ operator for non-deterministic variable assignments, imple-
mented by Algorithm 1 modified as discussed above, is a sound over-approx-
imation of the termination resilience semantics (cf. Figure 5):

**Proposition 1.** $\Lambda_{\text{tr}}[^l x := [c_1, c_2]]\gamma(t) \le \gamma(\text{ASSIGN}_T[^l x := [c_1, c_2]]t)$

*Resilience Join and Non-Tainted Program Variables.* At this point, one may be
tempted to extend the use of the resilience join to all variable assignments with a
non-tainted right-hand side expression (i.e., an expression that does not depend
on untrusted program variables) or, similarly, to *if* and *while* statements with
non-tainted boolean conditions. However, this change alone would be unsound.
Consider program *P* in Figure 1 and let the boolean condition at label 3 be
*`a * a >= 0`* where *a* is assigned with a non-deterministic value before *x*. Figure 13
shows the most precise decision trees that can be inferred at label 4 and 6.
At program label 3, the boolean condition *`a * a >= 0`* cannot be precisely rep-
resented by a (set of) linear constraints. Thus, no further constraints are added
before joining the trees. Since the decision tree at label 6 is totally defined (cf.
Figure 13b), using the resilience join would also yield a decision tree that is to-
tally defined (cf. Figure 7c), implying that termination resilience always holds.
<figure><img src="image_16.png" /><figcaption>Fig. 13: Abstract termination resilience semantics for program P.</figcaption></figure>

$$
\begin{align*}
\Lambda_{\text{tr}}^{\sharp}[\llbracket l \text{ skip} \rrbracket] t &\stackrel{\text{def}}{=} \text{SKIP}_T(t) \\
\Lambda_{\text{tr}}^{\sharp}[\llbracket l \text{ } := \mathbf{e} \rrbracket] t &\stackrel{\text{def}}{=} \text{ASSIGN}_T[\llbracket l \text{ } := \mathbf{e} \rrbracket](t) \\
\Lambda_{\text{tr}}^{\sharp}[\text{if}^l \mathbf{a} \triangleright 0 \{\mathbf{s}\}] t &\stackrel{\text{def}}{=} \Theta_{\text{tr}}^{\sharp}(t) \\
\Theta_{\text{tr}}^{\sharp} &\stackrel{\text{def}}{=} \lambda X.\text{FILTER}_T[\mathbf{a} \triangleright 0](\Lambda_{\text{tr}}^{\sharp}[\mathbf{s}]X) \gamma_T \text{ FILTER}_T[\mathbf{a} \not\triangleright 0](t) \\
\Lambda_{\text{tr}}^{\sharp}[\text{while}^l \mathbf{a} \triangleright 0 \{\mathbf{s}\}] t &\stackrel{\text{def}}{=} \text{LFP}^{\sharp} \Theta_{\text{tr}}^{\sharp} \\
\Lambda_{\text{tr}}^{\sharp}[\mathbf{s}_1; \mathbf{s}_2] t &\stackrel{\text{def}}{=} \Lambda_{\text{tr}}^{\sharp}[\mathbf{s}_2](\Lambda_{\text{tr}}^{\sharp}[\mathbf{s}_1])
\end{align*}
$$

<caption>Fig. 14: Abstract Program Semantics for Termination Resilience</caption>

However, program label 6 is not reachable and, indeed, termination resilience
does not hold: the program is robustly non-terminating when $x \le 0$.

To ensure soundness in the general case of non-tainted variables and expres-
sions, the resilience join should retain leaves labeled with a defined function only
when the domain partition that they represent is actually reachable. In practice,
we ensure this by conservatively under-approximating the weakest liberal pre-
condition of program statements by means of the approximation join [33]. We
leave finding less conservative approximations for future work.

**5.3 Abstract Termination Resilience Semantics.**

We can finally define in Figure 14 the abstract termination resilience semantics
$\Lambda_{\text{tr}}^{\sharp}[\mathbf{s}] : \mathcal{T} \to \mathcal{T}$ for each program statement $\mathbf{s}$. The `SKIP_T` operator simply increases by one the value of the functions labeling the leaves of the decision tree. The assignment operator `ASSIGN_T[\llbracket l \ x := \mathbf{e} \rrbracket]` is implemented by Algorithm 1, modified as discussed in Section 5.2 for non-deterministic variable assignments. The semantics of conditional `if` statements $\Theta_{\text{tr}}^{\sharp}$ employs the approximation join $\gamma_T$ as discussed above, after handling the boolean conditions with the `FILTER_T` operator (due to space limitations, we refer to [33] for its definition). The semantics for `while` loops iterates $\Theta_{\text{tr}}^{\sharp}$ with widening starting from the totally undefined decision tree `LEAF: $\perp_F$` until an abstract fixpoint is reached.

The abstract termination resilience semantics $\Lambda_{\text{tr}}^{\sharp}[\mathbf{p}] \in \mathcal{T}$ for a $\mathbf{p} \in \text{Prog}$ starts the termination resilience analysis with a decision tree containing a single leaf labeled with the zero function:
**Definition 5 (Abstract Termination Resilience Semantics).** Let $p \in \mathit{Prog}$ be a program. Its abstract termination resilience semantics is:

$$ \Lambda_{\mathrm{tr}}^{\mathfrak{h}}[\mathbf{p}] = \Lambda_{\mathrm{tr}}^{\mathfrak{h}}[\mathbf{s}^l] \stackrel{\mathrm{def}}{=} \Lambda_{\mathrm{tr}}^{\mathfrak{h}}[\mathbf{s}](\mathrm{LEAF}: 0). \qquad (9) $$

The termination resilience analysis is sound with respect to the approximation order $\leq$ (cf. Equation 8):

**Theorem 2 (Soundness).** $\Lambda_{\mathrm{tr}}[P] \leq \gamma(\Lambda_{\mathrm{tr}}^{\mathfrak{h}}[P])$

**Corollary 1 (Soundness).** $\Lambda[P] \in \mathcal{TR} \Leftrightarrow I \subseteq \mathrm{dom}(\gamma(\Lambda_{\mathrm{tr}}^{\mathfrak{h}}[P]))$

*Example 6.* Let us consider again $P_1$ in Figure 3a. Its most precise termination resilience semantics at label 3 matches the semantics of program $P$ at label 4 shown in Figure 13a. The assignment at label 2 – substituting $z$ with 10 and incrementing the value of the functions labeling the defined leaves – yields

<figure><img src="image_17.png" /></figure>

The assignment at label 1 yields LEAF: $\perp_F$. Its concretization $\gamma(\mathrm{LEAF}: \perp_F)$ is the totally undefined function $\emptyset$. We are thus unable to prove termination resilience. In this case, this is a true positive since indeed $\Lambda_{\mathrm{tr}}[P_1] \notin \mathcal{TR}$. $\triangleleft$

*Example 7.* Let us consider again program $P_2$ in Figure 3b. Its abstract termination resilience semantics at program label 3 is shown in Figure 11. The assignment at label 2 yields

<figure><img src="image_18.png" /></figure>

and the assignment at label 1 yields LEAF: $\perp_F$. We are again unable to prove termination resilience since $\gamma(\mathrm{LEAF}: \perp_F)$ is the totally undefined function $\emptyset$. This, however, is a false alarm since, in fact, $\Lambda_{\mathrm{tr}}[P_2] \in \mathcal{TR}$.

Let us consider instead the most precise abstract termination resilience semantics shown in Figure 13b. The assignment at label 2 yields

<figure><img src="image_19.png" /></figure>

and the assignment at label 1 then yields LEAF: $\omega$. In this case, we prove termination resilience since $\gamma(\mathrm{LEAF}: \omega)$ yields $\lambda\rho.\omega$, which is exactly $\Lambda_{\mathrm{tr}}[P_2]$. $\triangleleft$
# 6 Implementation and Experimental Evaluation

**Implementation.** We implemented our termination resilience analysis in the open-source tool FUNCTION-TR [26]. FUNCTION-TR is implemented in OCaml and relies on the APRON numerical abstract domain library [18] to manage decision tree constraints and functions labeling the tree leaves. It is also possible to activate the extension to lexicographic ranking functions [35], and tune the precision of the analysis by adjusting the widening delay. We use a simple implementation of the FILLT operation (cf. Section 5.2), which adds constraints, obtained from APRON's interval domain, bounding the values of the variables assigned with a non-deterministic value.

The analysis takes as input a numerical program written in a C-like syntax and outputs TRUE if all leaves of the inferred decision tree for the program are labelled with defined functions, i.e., Termination Resilience holds for any initial program state. Otherwise, it outputs UNKNOWN to indicate that Robust Non-Termination may hold (i.e., FUNCTION-TR raises a potential Robust Non-Termination alarm). In this case, the defined partitions of the inferred decision tree are a sufficient precondition for Termination Resilience.

**Experimental Evaluation.** Note that always terminating programs trivially satisfy Termination Resilience. For this reason, in our evaluation, we deliberately focus on programs that admit both terminating and non-terminating executions, thereby targeting the class of benchmarks where termination resilience is a non-trivial property and where our analysis can be meaningfully evaluated.

We selected a total of 62 programs from three sources: SV-COMP 2024¹, the benchmarks of the state-of-the-art non-termination analyzer Pulse [29], and the recent survey on non-termination bugs by Shi et al. [30]. From SV-COMP, we collected 39 programs from the sets termination-crafted-lit, termination-restricted-15, and termination-nla in the Termination category, all labeled as non-terminating in the associated .yml files (average length of 23 lines of code). From the Pulse benchmarks [29] we retained 10 programs (averaging 20 lines of code), and from the survey benchmarks [30] we retained 13 (averaging 25 lines of code – each program is a simplified extract derived from real-world open-source software that exhibited a non-termination bug). We excluded 16 (resp. 36) always terminating programs from these two latter sources. Furthermore, we discarded 33 (resp. 42) programs making use of pointers, bitwise operations, or recursive functions, which are currently not fully supported by our prototype tool.

We constructed variants of these 62 programs, for all possible combinations of variable initializations (e.g., `__VERIFYER_nondet_int()` for programs in SV-COMP) with untrusted (input) or trusted (`[-∞, +∞]`) values. In doing so, we obtained a benchmark of 278 test cases (150 from SV-COMP, 42 from Pulse [29], 86 from Shi et al. [30]). Note that variable initializations also occur within loops for 54 of 278 test cases (28 from SV-COMP, 12 from Pulse [29], 14 from Shi et al. [30]). The experiments were conducted on a 64-bit 8-Core CPU (AMD® Ryzen

<footnote n="1">¹ https://sv-comp.sosy-lab.org/2024/</footnote>
<table><caption>Table 1: Evaluation results.</caption><thead><tr><th>Benchmark</th><th>Configuration</th><th>Property</th><th>Verified</th><th>Alarms</th><th>TO</th><th>Time (s)</th></tr></thead><tbody><tr><td rowspan="2">SV-COMP</td><td rowspan="2">FUNCTION-TR-Boxes</td><td>Termination</td><td>0</td><td>150</td><td>0</td><td>3.0</td></tr><tr><td>Termination Resilience</td><td>58</td><td>92</td><td>0</td><td>3.0</td></tr><tr><td rowspan="2">FUNCTION-TR-Polyhedra</td><td rowspan="2">FUNCTION-TR-Boxes</td><td>Termination</td><td>0</td><td>150</td><td>0</td><td>6.0</td></tr><tr><td>Termination Resilience</td><td>99</td><td>51</td><td>0</td><td>14.0</td></tr><tr><td rowspan="2">Pulse [29]</td><td rowspan="2">FUNCTION-TR-Boxes</td><td>Termination</td><td>0</td><td>42</td><td>0</td><td>0.5</td></tr><tr><td>Termination Resilience</td><td>23</td><td>19</td><td>0</td><td>0.5</td></tr><tr><td rowspan="3">Shi et al. [30]</td><td rowspan="3">FUNCTION-TR-Polyhedra</td><td>Termination</td><td>0</td><td>42</td><td>0</td><td>7.0</td></tr><tr><td>Termination Resilience</td><td>23</td><td>19</td><td>0</td><td>17.0</td></tr><tr><td>Termination</td><td>0</td><td>86</td><td>0</td><td>2.0</td></tr><tr><td rowspan="2"></td><td rowspan="2">FUNCTION-TR-Boxes</td><td>Termination</td><td>0</td><td>28</td><td>0</td><td>2.0</td></tr><tr><td>Termination Resilience</td><td>58</td><td>28</td><td>0</td><td>2.0</td></tr><tr><td rowspan="2"></td><td rowspan="2">FUNCTION-TR-Polyhedra</td><td>Termination</td><td>0</td><td>86</td><td>0</td><td>54.0</td></tr><tr><td>Termination Resilience</td><td>58</td><td>20</td><td>8</td><td>257.0</td></tr></tbody></table>

7 pro 5850u) with 16GB of RAM on Ubuntu 20.04. Note that, for the moment, our tool is single-threaded and uses only one CPU core.

Table 1 summarizes the results of the evaluation with FUNCTION-TR configured to use the boxes (FUNCTION-TR-Boxes) or polyhedra (FUNCTION-TR-Polyhedra) abstract domain to manage decision tree constraints. We configured the analysis to perform widening after two iterations, and we left the extension with lexicographic functions disabled. We used a timeout of 120s (wall time) per test case. Activating the extension or increasing the widening delay makes no difference on these benchmarks aside from an increased execution time. As expected, proving Termination Resilience instead of Termination (i.e., Termination Resilience where all variables are considered untrusted) considerably reduces the number of alarms, almost 65% using decision tree with polyhedral constraints. This shows that our termination resilience analysis is an effective way to triage and prioritize alarms related to program non-termination. The execution time reported in the last column of Table 1 corresponds to the total analysis time over all test cases that did not time out.

The full comparison between FUNCTION-TR-Boxes and FUNCTION-TR-Polyhedra is shown in Figure 15, where the axes denote execution (wall) time in seconds, and green stars (★) label test cases where the configurations have the same precision (i.e., both prove Termination Resilience or raise an alarm), while red crosses (x) and blue circles (●) label test cases where FUNCTION-TR-Polyhedra and FUNCTION-TR-Boxes are more precise (i.e., prove Termination Resilience for more test cases), respectively. The presence of blue circles may be surprising: in few test cases, using a more precise numerical domain to manage decision

<figure><img src="image_20.png" /><figcaption>Fig. 15: FUNCTION-TR-Boxes vs FUNCTION-TR-Polyhedra.</figcaption></figure>
tree constraints actually causes a loss of precision when widening is performed (because the widening heuristic leverages adjacent decision tree partitions, and more partitions are formed with more precise decision tree constraints), while using a less precise numerical domain allows the widening to generalize better. We leave the implementation of better widening heuristics [8] for future work.

*Triage of Alarms Found by Non-Termination Analyzers.* We evaluated the ability of FUNCTION-TR to filter out non-critical non-termination alarms found by the non-termination analyzers Pulse, Dynamite and Ultimate-Automizer.

We reused the benchmark in which Raad et al. [29] reported non-termination bugs found by Pulse and Dynamite [21]. The programs in this benchmark use non-linear arithmetic and are extracted from the set *termination-nla* in the Termination category of SV-COMP. We excluded 9 out of 40 non-terminating programs that rely on unsigned int, since we assume a mathematical integer semantics. As in the previous evaluation, for each test filename.c, we generated variants for each possible combination of variable initialization which gave us 86 programs to test (with an average of 54 lines of code). In addition to the result of [29], we also ran the non-termination analysis of Ultimate-Automizer [7].

In Table 2, the suffixes of the test names, generated by the regular expression $-[r + i]*$, describe the sequence of variable initializations. For instance the test filename-ri.c is the variant of filename.c in which we used a trusted (non-deterministic) value ($[-\infty, +\infty]$) for the first variable initialization and an untrusted (input) value for the second. A non-termination bug found by Pulse (column P in Table 2), Dynamite (column D in Table 2) or Ultimate-Automizer (column U in Table 2) is denoted $\Delta$, an empty cell indicates that the tool is inconclusive. Note that the tool results should not be compared as they consider different integer semantics. For FUNCTION-TR, ✓ means that it proved Termination Resilience (returns TRUE), while $!(FP)$ or $!(TP)$ denotes the cases where FUNCTION-TR raised a false alarm (upon manual inspection, Termination Resilience, in fact, holds) or a true alarm (upon manual inspection, Termination Resilience indeed does not hold), respectively.

From this evaluation, we conclude that our prototype FUNCTION-TR is able to filter out non-critical non-termination alarms found by non-termination analyzers. More precisely, Termination Resilience is proved for 16 programs where Pulse or Dynamite or Ultimate-Automizer found a non-terminating execution, hence FUNCTION-TR removes 16 alarms. Moreover, Termination Resilience is proved for 4 programs where Pulse, Dynamite and Ultimate-Automizer did not find any non-termination bug. Finally, by manual inspection, we report that 58 out of the 62 alarms raised by FUNCTION-TR are true positives. This result was expected: most of the non-terminating programs from the SV-COMP category *termination-nla* are constructed from terminating ones by making them always diverging, which is a case of Robust Non-Termination where FUNCTION-TR must raise an alarm. Dually, 4 of the 62 alarms are false positives. In our benchmark it is mostly due to the inherited imprecision of the decision tree abstract domain on programs exhibiting non-linear arithmetic operations or, more frequently, when the widening operator does not generalize well.
<table><caption>Table 2: Triage of non-termination alarms by FUNCTION-TR.</caption><thead><tr><th>Test Case</th><th>P</th><th>D</th><th>U</th><th>FUNCTION-TR</th></tr></thead><tbody><tr><td>bresenham1-both-nt-ii</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>bresenham1-both-nt-ir</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>bresenham1-both-nt-ri</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>bresenham1-both-nt-rr</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-i</td><td>▲▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-r</td><td>▲▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>cohencul-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>dijkstra1-both-nt-i</td><td>▲</td><td>▲</td><td></td><td>!{TP}</td></tr><tr><td>dijkstra1-both-nt-r</td><td>▲</td><td>▲</td><td></td><td>✓</td></tr><tr><td>dijkstra2-both-nt-i</td><td>▲</td><td>▲</td><td></td><td>!{TP}</td></tr><tr><td>dijkstra2-both-nt-r</td><td>▲</td><td>▲</td><td></td><td>✓</td></tr><tr><td>dijkstra3-both-nt-i</td><td>▲</td><td>▲</td><td></td><td>!{TP}</td></tr><tr><td>dijkstra3-both-nt-r</td><td>▲</td><td>▲</td><td></td><td>✓</td></tr><tr><td>dijkstra4-both-nt-i</td><td>▲</td><td>▲</td><td></td><td>!{TP}</td></tr><tr><td>dijkstra4-both-nt-r</td><td>▲</td><td>▲</td><td></td><td>✓</td></tr><tr><td>dijkstra5-both-nt-i</td><td>▲</td><td>▲</td><td></td><td>!{TP}</td></tr><tr><td>dijkstra5-both-nt-r</td><td>▲</td><td>▲</td><td></td><td>✓</td></tr><tr><td>dijkstra4-both-nt-i</td><td>▲</td><td>▲</td><td></td><td>!{TP}</td></tr><tr><td>dijkstra4-both-nt-r</td><td>▲</td><td>▲</td><td></td><td>✓</td></tr><tr><td>dijkstra6-both-nt-i</td><td>▲</td><td>▲</td><td></td><td>!{TP}</td></tr><tr><td>egcd2-both-nt-ii</td><td>▲▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>egcd2-both-nt-ir</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>egcd2-both-nt-ri</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>egcd2-both-nt-rr</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>egcd3-both-nt-ii</td><td>▲▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>egcd3-both-nt-ir</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>egcd3-both-nt-ri</td><td>▲▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>egcd3-both-nt-rr</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>egcd-both-nt-ii</td><td>▲▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>egcd-both-nt-ir</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>egcd-both-nt-ri</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>egcd-both-nt-rr</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>freire1-both-nt-i</td><td>▲</td><td></td><td></td><td>!{TP}</td></tr><tr><td>freire1-both-nt-r</td><td>▲</td><td></td><td></td><td>!{TP}</td></tr><tr><td>geo1-both-nt-ii</td><td>▲</td><td></td><td></td><td>!{TP}</td></tr></tbody></table><table><thead><tr><th>Test Case</th><th>P</th><th>D</th><th>U</th><th>FUNCTION-TR</th></tr></thead><tbody><tr><td>geo1-both-nt-ir</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo1-both-nt-ri</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo1-both-nt-rr</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo2-both-nt-ii</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo2-both-nt-ir</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo2-both-nt-ri</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo2-both-nt-rr</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo3-both-nt-ii</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo3-both-nt-ir</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo3-both-nt-ri</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>geo3-both-nt-rr</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>hard2-both-nt-i</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>hard2-both-nt-r</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>hard2-both-nt-ii</td><td>▲▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>hard2-both-nt-ir</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>hard2-both-nt-ri</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>hard2-both-nt-rr</td><td>▲▲</td><td></td><td>▲</td><td>✓</td></tr><tr><td>prod4br-both-nt-ii</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>prod4br-both-nt-ir</td><td></td><td></td><td></td><td>✓</td></tr><tr><td>prod4br-both-nt-ri</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>prod4br-both-nt-rr</td><td></td><td></td><td></td><td>✓</td></tr><tr><td>prodbin-both-nt-ii</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>prodbin-both-nt-ir</td><td></td><td></td><td></td><td>✓</td></tr><tr><td>prodbin-both-nt-ri</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>prodbin-both-nt-rr</td><td></td><td></td><td></td><td>✓</td></tr><tr><td>ps2-both-nt-i</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>ps2-both-nt-r</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>ps3-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>ps3-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>ps4-both-nt-i</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>ps4-both-nt-r</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>ps5-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>ps5-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>ps6-both-nt-i</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>ps6-both-nt-r</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>sqrt1-both-nt-i</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>sqrt1-both-nt-r</td><td>▲</td><td></td><td>▲</td><td>!{TP}</td></tr><tr><td>sqrt2-both-nt-ii</td><td></td><td></td><td></td><td>!{TP}</td></tr><tr><td>sqrt2-both-nt-ir</td><td></td><td></td><td></td><td>!{FP}</td></tr><tr><td>sqrt2-both-nt-ri</td><td></td><td></td><td></td><td>!{FP}</td></tr><tr><td>sqrt2-both-nt-rr</td><td></td><td></td><td></td><td>!{FP}</td></tr></tbody></table>

*Data Availability.* The instrumented programs used for the experimental evaluation are provided (alongside with the tool) in our artifact on Zenodo [26].

# 7 Related Work

Several approaches have been proposed in the literature to prove program termination [3,2,4,6,14,23,24,19, etc.], or the existence of diverging executions (potential non-termination) in programs [29,37,17,5,21,22,20,19, etc.]. However, to the best of our knowledge, none of the other works studies termination or non-termination in the presence of untrusted inputs and trusted variables. We believe an interesting avenue for future research is to extend these approaches, with the aim of developing new methods to prove Termination Resilience or the existence of Robust Non-Termination bugs.

This work is inspired by the work of Girol et al. [15,16], where they introduce the notion of Robust Reachability of a safety bug. They additionally propose symbolic execution and bounded model checking techniques to find robustly reachable bugs. Instead, we introduce the notion of Robust Non-Termination, the
robust occurrence of a *liveness* bug, and its negation Termination Resilience. We propose a static analysis approach to verify Termination Resilience and detect potential Robust Non-Termination bugs.

In a similar spirit as Girol et al., Parolini and Miné have introduced the notion of *safety* Non-Exploitability [28,27] and proposed a static analysis, combining taint and reachable values information, to prove that the untrusted inputs (called an attacker in their work) cannot trigger or silence a safety bug in a program. In our work, we focus on *liveness* bugs (notably, non-termination bugs) and we are only concerned with the untrusted inputs triggering these bugs, not silencing them. We also observe that the analysis of Parolini and Miné assumes full knowledge of trusted variables values at the time untrusted inputs values are chosen. In contrast, our semantic and static analysis frameworks naturally accommodate models with incomplete knowledge, including blind models in which the values of the untrusted inputs are chosen before the values of the trusted variables are observed (as in the programs in Figure 3).

Our work builds on the decision tree abstract domain [33,34] and inherits its imprecision (cf. Section 6). It also means that we could benefit from the extensions of the domain. Urban et al. [36] proposed a static analysis of CTL properties using the decision trees abstract domain augmented with the new abstract operators. Later, Moussaoui-Remil et al. [25], proposed an analysis operating on decision trees to infer minimal sets of variables that need to be constrained in order to ensure a CTL property. We could leverage this work to infer minimal sets of untrusted variables that need to be strained to ensure termination resilience.

Termination Resilience can be formulated within the Alternating-Time Temporal Logic (ATL) [1] whose formulas are the same as those of CTL (in which termination is expressible), except that the universal (A) and existential (E) operators are generalized with a selective quantifier $\langle\langle\cdot,\rangle\rangle$ over paths that are possible outcomes of games. Given $n$ players $p_1, \dots, p_n$, a program satisfies $\langle\langle p_1, \dots, p_n \rangle\rangle \phi$ if and only if there exists a strategy for the $n$ players to force the program to satisfy $\phi$. Termination Resilience is expressed as the existence of a strategy for the trusted variables that ensures program termination. Hence, an abstract interpretation of ATL properties seems to be a natural generalization of our work toward an analysis of resilience CTL properties.

# 8 Conclusion and Future Work

We have proposed a novel program property, called Termination Resilience, and an abstract interpretation-based static analysis to infer sufficient preconditions ensuring it. To this end, we have enhanced the decision tree abstract domain of piecewise-defined functions [33,34] with non-trivial transformer operators. In our evaluation, we have shown that our static analysis is able to reduce by almost 65% the alarms related to program non-termination.

For future work, an interesting direction is a static analysis for ATL properties with an initial focus on the resilience of CTL properties. We also plan to extend the analysis to data structure-manipulating programs.
References

1. Rajeev Alur, Thomas A Henzinger, and Orna Kupferman. Alternating-time temporal logic. *Journal of the ACM (JACM)*, 49(5):672–713, 2002.

2. Dirk Beyer, Matthias Dangl, Daniel Dietsch, and Matthias Heizmann. Correctness witnesses: exchanging verification results between verifiers. In Thomas Zimmermann, Jane Cleland-Huang, and Zhendong Su, editors, *Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016*, pages 326–337. ACM, 2016.

3. Dirk Beyer, Matthias Dangl, Daniel Dietsch, Matthias Heizmann, and Andreas Stahlbauer. Witness validation and stepwise testification across software verifiers. In Elisabetta Di Nitto, Mark Harman, and Patrick Heymans, editors, *Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, Bergamo, Italy, August 30 - September 4, 2015*, pages 721–733. ACM, 2015.

4. Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. Safety verification and refutation by k-invariants and k-induction. In Sandrine Blazy and Thomas P. Jensen, editors, *Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings*, volume 9291 of *Lecture Notes in Computer Science*, pages 145–161. Springer, 2015.

5. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. Proving non-termination by program reversal. In Stephen N. Freund and Eran Yahav, editors, *PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021*, pages 1033–1048. ACM, 2021.

6. Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, and Björn Wachter. Bit-precise procedure-modular termination analysis. *ACM Trans. Program. Lang. Syst.*, 40(1):1:1–1:38, 2018.

7. Yu-Fang Chen, Matthias Heizmann, Ondřej Lengál, Yong Li, Ming-Hsien Tsai, Andrea Turrini, and Lijun Zhang. Advanced automata-based algorithms for program termination checking. In *Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation*, pages 135–150, 2018.

8. Nathanaël Courant and Caterina Urban. Precise Widening Operators for Proving Termination by Abstract Interpretation. In Axel Legay and Tiziana Margaria, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I*, volume 10205 of *Lecture Notes in Computer Science*, pages 136–152, 2017.

9. Patrick Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. *Theoretical Computer Science*, 277(1-2):47–103, 2002.

10. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, *Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977*, pages 238–252. ACM, 1977.

11. Patrick Cousot and Radhia Cousot. Abstract Interpretation Frameworks. *Journal of Logic and Computation*, 2(4):511–547, 1992.
12. Patrick Cousot and Radhia Cousot. An Abstract Interpretation Framework for Termination. In John Field and Michael Hicks, editors, *Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012*, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 245–258. ACM, 2012.

13. Robert W. Floyd. Assigning Meanings to Programs. *Proceedings of Symposium on Applied Mathematics*, 19:19–32, 1967.

14. Mirco Giacobbe, Daniel Kroening, and Julian Parsert. Neural termination analysis. In Abhik Roychoudhury, Cristian Cadar, and Miryung Kim, editors, *Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022*, Singapore, Singapore, November 14-18, 2022, pages 633–645. ACM, 2022.

15. Guillaume Girol, Benjamin Farinier, and Sébastien Bardin. Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference. In Alexandra Silva and K. Rustan M. Leino, editors, *Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I*, volume 12759 of *Lecture Notes in Computer Science*, pages 669–693. Springer, 2021.

16. Guillaume Girol, Benjamin Farinier, and Sébastien Bardin. Introducing robust reachability. *Formal Methods Syst. Des.*, 63(1):206–234, 2024.

17. Jera Hensel, Constantin Mensendiek, and Jürgen Giesl. Aprove: Non-termination witnesses for C programs - (competition contribution). In Dana Fisman and Grigore Rosu, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022*, Munich, Germany, April 2-7, 2022, *Proceedings, Part II*, volume 13244 of *Lecture Notes in Computer Science*, pages 403–407. Springer, 2022.

18. Bertrand Jeannet and Antoine Miné. Apron: A library of numerical abstract domains for static analysis. In Ahmed Bouajjani and Oded Maler, editors, *Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings*, volume 5643 of *Lecture Notes in Computer Science*, pages 661–667. Springer, 2009.

19. Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada. HFL(Z) validity checking for automated program verification. *Proc. ACM Program. Lang.*, 7(POPL):154–184, 2023.

20. Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio. Proving non-termination using max-smt. In Armin Biere and Roderick Bloem, editors, *Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings*, volume 8559 of *Lecture Notes in Computer Science*, pages 779–796. Springer, 2014.

21. Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, and ThanhVu Nguyen. Dynamite: dynamic termination and non-termination proofs. *Proc. ACM Program. Lang.*, 4(OOPSLA):189:1–189:30, 2020.

22. Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin. Termination and non-termination specification inference. In David Grove and Stephen M. Blackburn, editors, *Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015*, pages 489–498. ACM, 2015.
23. Viktor Malík, Frantisek Necas, Peter Schrammel, and Tomás Vojnar. 2ls: Arrays and loop unwinding - (competition contribution). In Sriram Sankaranarayanan and Natasha Sharygina, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II*, volume 13994 of *Lecture Notes in Computer Science*, pages 529-534. Springer, 2023.

24. Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, R. Venkatesh, and Supratik Chakraborty. PROTON: probes for termination or not (competition contribution). In Bernd Finkbeiner and Laura Kovács, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III*, volume 14572 of *Lecture Notes in Computer Science*, pages 393-398. Springer, 2024.

25. Naïm Moussaoui Remil, Caterina Urban, and Antoine Miné. Automatic detection of vulnerable variables for CTL properties of programs. In Nikolaj S. Bjørner, Marijn Heule, and Andrei Voronkov, editors, *LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024*, volume 100 of *EPiC Series in Computing*, pages 116-126. EasyChair, 2024.

26. Naïm Moussaoui Remil and Caterina Urban. Termination resilience static analysis (artifact). https://zenodo.org/records/17176433, 2025.

27. Francesco Parolini. *Static Analysis for Security Properties of Software by Abstract Interpretation. (Analyse statique des propriétés de sécurité des logiciels par interprétation abstraite)*. PhD thesis, Sorbonne University, Paris, France, 2024.

28. Francesco Parolini and Antoine Miné. Sound Abstract Nonexploitability Analysis. In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors, *Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II*, volume 14500 of *Lecture Notes in Computer Science*, pages 314-337. Springer, 2024.

29. Azalea Raad, Julien Vanegue, and Peter W. O'Hearn. Non-termination proving at scale. *Proc. ACM Program. Lang.*, 8(OOPSLA2):246-274, 2024.

30. Xiuhan Shi, Xiaofei Xie, Yi Li, Yao Zhang, Sen Chen, and Xiaohong Li. Large-scale analysis of non-termination bugs in real-world OSS projects. In Abhik Roychoudhury, Cristian Cadar, and Miryung Kim, editors, *Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18, 2022*, pages 256-268. ACM, 2022.

31. Alan Turing. Checking a Large Routine. In *Report of a Conference on High Speed Automatic Calculating Machines*, pages 67-69, 1949.

32. Caterina Urban. FuncTion: An Abstract Domain Functor for Termination - (Competition Contribution). In Christel Baier and Cesare Tinelli, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings*, volume 9035 of *Lecture Notes in Computer Science*, pages 464-466. Springer, 2015.

33. Caterina Urban. *Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs* (Analyse Statique par Interprétation Abstraite de Pro-
priétés Temporelles Fonctionnelles des Programmes). PhD thesis, École Normale Supérieure, Paris, France, 2015.

34. Caterina Urban and Antoine Miné. A Decision Tree Abstract Domain for Proving Conditional Termination. In Markus Müller-Olm and Helmut Seidl, editors, *Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings*, volume 8723 of Lecture Notes in Computer Science, pages 302–318. Springer, 2014.

35. Caterina Urban and Antoine Miné. An Abstract Domain to Infer Ordinal-Valued Ranking Functions. In Zhong Shao, editor, *Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings*, volume 8410 of Lecture Notes in Computer Science, pages 412–431. Springer, 2014.

36. Caterina Urban, Samuel Ueltschi, and Peter Müller. Abstract interpretation of CTL properties. In Andreas Podelski, editor, *Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings*, volume 11002 of Lecture Notes in Computer Science, pages 402–422. Springer, 2018.

37. Yao Zhang, Xiaofei Xie, Yi Li, Sen Chen, Cen Zhang, and Xiaohong Li. Endwatch: A practical method for detecting non-termination in real-world software. In *2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)*, pages 686–697. IEEE, 2023.