F Largilliere

E Coevoet

L Grisoni

C Duriez

Real-time FEM based control of soft surgical robots

Introduction

Surgical robots, such as the Da Vinci c , interact with delicate biological structures such as blood vessels or internal organs. However, they are made of rigid materials that limit their ability of moving through confined spaces without inducing excessive contact pressures and stress concentrations which could create new injuries. An alternative solution, potentially easier to produce and suitable for interventions where the highest precision (less than a few millimeters) is not necessary, is growing in the scientific community with the development of robots made of soft materials [START_REF] Majidi | Soft robotics: A perspective -Current trends and prospects for the future[END_REF]. This type of robots allows for a safer contact with internal organs and displacement among them at the cost of an increase in the complexity of control. Indeed, soft robots can dissipate the energy of collision and comply with the shape of their environment through their internal deformation. However, their infinite number of degrees of freedom does not allow to compute inverse kinematics easily. Also, the idea of using a large number of actuators to simplify the control is countered by the fact that these actuators are coupled together through the whole deformation of the robot.

Although soft, these robots could still be used in situations where medical instruments need to stay in a fixed position, by rigidifying a robot filled with particles jammed through vacuum actuation [START_REF] Jiang | The Core-Snake, the variable stiffness laparoscopic camera in The Hamlyn Symposium on Medical Robotics[END_REF] .

To address the problem of controlling these robots, traditional robotic methods cannot be used because the coupling between actuators and effectors is constantly modified through the deformation of the robot. This is why it is necessary to know the influence of applied forces on the structure while controlling it. In this purpose, we have developed a new method of control [START_REF] Duriez | Control of Elastic Soft Robots based on Real-Time Finite Element Method[END_REF] based on the real-time inverse simulation with internal deformation computed through the use of Finite Element Method (FEM). It was coded in SOFA, an open-source framework that contains fast implementations of FEM as well as optimization methods for collision response and mechanical interactions with haptic feedback. This work has demonstrated its first proofs on various numerical examples but also on a real deformable robot made of silicone and actuated through cables.

To model the large non-linear deformations undergone by the soft structure, a corotational volume FEM formulation [START_REF] Felippa | A systematic approach to the element-independent corotational dynamics of finite elements[END_REF] is used in this work. At each step i of the real-time simulation, the internal forces are linearized as follows:

f (x i ) ≈ f (x i-1 ) + K(x i-1 )dx (1)
where f represents the volumetric internal stiffness forces at a given position x of the nodes, K(x) is the tangent stiffness matrix that depends on the actual position of the nodes and dx is the displacement of nodes between two steps dx = x i -x i-1 .

In a first approach, we want the model to be in static equilibrium state regarding internal and external forces, which is acceptable for quasi-static motions i.e for low velocities. The following equation has then to be solved:

-K(x i-1 )dx = p + f (x i-1 ) + J T λ.
(

) 2
where p represents the external forces (e.g. gravity) and J T λ gathers the contributions of the actuators through a product between J T and λ that are respectively the direction of the forces and their unknown intensities.

Then, we use the following algorithm :

-First, a free configuration is found by solving the previous equation with λ = 0. We can then compute the violation of the desired positions before the appropriate actuation. -Secondly, the following projection into constraint space is used :

δ = JK -1 J T W λ + δ free (3)
where δ free and δ are respectively the violations before actuation and the one after actuation i.e to be minimized by the control. A Gauss-Seidel iterative solver is used to find a solution for the couple (λ,δ) -Finally, the free configuration of the robot is updated according to the influence of the forces J T λ previously calculated to obtain the configuration under actuation.

The constraint on the terminal actuator is set by assigning its three directions of displacement (x, y and z) and forcing λ at zero, as a non-directly actuated point. This formulation of the problem allows for various actuators to be modeled by taking into account their physical characteristics (directional of actuation, unilateral (e.g pulling cable)/bilateral actuation, limited stroke) through the use of bilateral or unilateral constraints. Pneumatic actuation can also be used via normal constraint applied to selected faces of the deformable cavity.

Coupling with soft-tissue models

When using FEM, it is usual to impose the load and get the displacements (or deformations), which could be considered as a direct mechanical model in robotics. On the contrary, what the algorithm presented here does is a novel use of FEM to obtain an inverse mechanical model. However, taking into account all degrees of freedom of the model would be too much expensive for the algorithm to be real-time. This is why a compliance matrix W condensed in the constraint space is used. This matrix holds only the modeling of the mechanical coupling between each actuator and effector (or other actuators) so that it can be used in the inverse algorithm computed fast enough to be efficient.

With very small changes in the algorithms, [START_REF] Coevoet | Introducing interactive inverse FEM simulation and its application for adaptive radiotherapy[END_REF] uses the method for parametrization of soft-tissue models by inverse simulation. It is applied to semi-automatic registration for adaptive radiotherapy. Indeed, the same condensation strategy is used to find the parameters and the boundary conditions (physics-based external loads) that provide the displacements that are observed on the images. This strategy is very important in the context of the navigation of a surgical soft robot interacting with the soft-tissue environment of the patient (see figure 1) The presentation will show how we envision to couple this inverse FEM method to provide online both control of the robot and registration of a physicsbased model of the patient. This work presents the use of a FEM inverse model, computed in real-time to control the motion of the soft robot. We also show that this inverse model strategy can be used to parametrize the modeling of the soft tissues of a patient by registration of the deformations. From these works, we can consider the development of a real-time simulation that could be used during a surgical intervention to control a soft robot that could navigate among organs whose positions and properties would be updated and taken in consideration while choosing how to plan the movements of the robot and how to actuate it. Another possible application is the control of soft robotic organs for realistic surgery training.

Fig. 1 .

 1 Fig. 1. The concept of a soft laparoscopic robot. Thanks to its flexibility, the robot can access difficult areas, while preventing hard contact stress with the wall of the soft tissues. Both patient anatomy deformations and soft robot would require FEM inverse method


Caterina Urban
email: urban@di.ens.fr

Antoine Miné
email: mine@di.ens.fr

To Infinity... and Beyond! *

Keywords: 1998 ACM Subject Classification D.2.4 Software/Program Verification, F.3.1 Specifying and Verifying and Reasoning about Programs, F.3.2 Semantics of Programming Languages Abstract Interpretation, Ranking Function, Ordinals, Termination Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

The traditional method for proving program termination consists in inferring a ranking function. In many cases (i.e., programs with unbounded non-determinism), a single ranking function over natural numbers is not sufficient. Hence, we propose a new abstract domain to automatically infer ranking functions over ordinals. We extend an existing domain for piecewise-defined natural-valued ranking functions to polynomials in ω, where the polynomial coefficients are natural-valued functions of the program variables. The abstract domain is parametric in the choice of the state partitioning inducing the piecewise-definition and the type of functions used as polynomial coefficients. To our knowledge this is the first abstract domain able to reason about ordinals. Handling ordinals leads to a powerful approach for proving termination of imperative programs, which in particular allows us to take a first step in the direction of proving termination under fairness constraints and proving liveness properties of (sequential and) concurrent programs.

Introduction

The traditional method for proving program termination [START_REF] Floyd | Assigning Meanings to Programs[END_REF] consists in inferring ranking functions, namely mappings from program states to elements of a well-ordered set (e.g., ordinals) whose value decreases during program execution.

Intuitively, we can define a partial ranking function from the states of a program to ordinals in an incremental way: we start from the program final states, where the function has value 0 (and is undefined elsewhere); then, we retrace the program backwards enriching the domain of the function with the co-reachable states mapped to the maximum number of program steps until termination. In [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], this intuition is formalized into a most precise ranking function that can be expressed in fixpoint form by abstract interpretation [START_REF] Cousot | Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF] of the program maximal trace semantics.

However, the most precise ranking function is not computable. In [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF], we present a decidable abstraction for imperative programs by means of piecewise-defined ranking functions over natural numbers. These functions are attached to the program control points and represent an upper bound on the number of program execution steps remaining before termination. Nonetheless, in many cases (i.e., programs with unbounded non-determinism), natural-valued ranking functions are not powerful enough. For this reason, we propose a new abstract domain to automatically infer ranking functions over ordinals.

We extend the abstract domain of piecewise-defined natural-valued ranking functions to piecewisedefined ordinal-valued ranking functions represented as polynomials in ω, where the polynomial coefficients are natural-valued functions of the program variables. The domain automatically infers such ordinal-valued functions through backward invariance analysis. To handle disjunctions arising from tests and loops, the analysis automatically partitions the space of values for the program variables into abstract program states, inducing a piecewise definition of the functions. Moreover, the domain naturally infers sufficient preconditions for program termination. The analysis is sound: all program executions respecting these sufficient preconditions are indeed terminating, while an execution that does not respect these conditions might not terminate.

The abstract domain is parametric in the choices of the state abstraction used for partitioning (in particular, we can abstract the program states using any convex abstract domain such as intervals [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagons [START_REF] Miné | The Octagon Abstract Domain[END_REF], polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF], . . . ) and the type of functions used as polynomial coefficients (e.g., affine, quadratic, cubic, exponential, . . . ).

To our knowledge this is the first abstract domain able to reason about ordinals. Handling ordinals leads to a powerful approach for proving termination of imperative programs, which in particular allows us to take a first step in the direction of proving termination under fairness constraints and proving liveness properties of (sequential and) concurrent programs.

Ordinal-Valued Ranking Functions

We derive a decidable program termination semantics by abstract interpretation of the program most precise ranking function [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF]: first, we introduce the abstract domain O of ordinal-valued functions; then, in the next section, we employ state partitioning to lift this abstraction to piecewise-defined functions [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF].

Let X be a finite set of program variables. We split the program state space Σ L×E into program control points L and environments E X → Z, which map each program variable to an integer value. No approximation is made on L. On the other hand, each program control point l ∈ L is associated with an element o ∈ O of the abstract domain O. Specifically, o represents an abstraction of the partial function γ O (o) ∈ E ⇀ O defined on the environments related to the program control point l:

E ⇀ O,⊑ γ O ←-O,⊑ O .
Intuitively, where defined, the partial function provides a ranking function proving (definite) termination; where undefined, it denotes (potential) non-termination.

Natural-Valued Functions. We assume we are given an abstraction S,⊑ S of environments: P(E),⊆ γ S ←-S,⊑ S (i.e., any abstract domain such as intervals [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagons [START_REF] Miné | The Octagon Abstract Domain[END_REF], convex polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF], . . . ), and an abstraction S ×F,⊑ F of E ⇀ O,⊑ by means of natural-valued functions of the program variables: E ⇀ O,⊑ γ F ←-S × F,⊑ F . More specifically, the abstraction S × F,⊑ F encodes a partial function v ∈ E ⇀ O by a pair s,f of a natural-valued (total) function (e.g., an affine function [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF]) f ∈ F and an abstract state s ∈ S which restricts its domain. For instance, [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF][START_REF] Edsger | A Discipline of Programming[END_REF],3x+2 denotes the affine function 3x+2 restricted to the interval [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF][START_REF] Edsger | A Discipline of Programming[END_REF]. We can now use the abstractions S and F to build the abstract domain O.

Ordinal-Valued Functions. The elements of the abstract domain

O belong to O S ×W where W {⊥ W } ∪ { i ω i • f i | f i ∈ F} ∪ {⊤ W }
is the set of ordinal-valued ranking functions of the program variables (in addition to the function ⊥ W representing potential non-termination, and the function ⊤ W representing the lack of enough information to conclude1 ). More specifically, an abstract function o ∈ O is a pair of an abstract state s ∈ S and a polynomial in ω (i.e., an ordinal in Cantor Normal Form)

ω k •f k +•••+ω 2 •f 2 +ω•f 1 +f 0 where the coefficients f 0 ,f 1 ,f 2 ,...,f k belong to F. Note that the ordinal ω k •f k +•••+ω 2 •f 2 +ω•f 1 +f 0 is isomorphic to the lexicographic tuple (f k ,...,f 1 ,f 0 ).
In fact, our abstract domain is isomorphic to the set of all lexicographic ranking functions with finite (but unbounded) number of components. In the following, with abuse of notation, we use a map s → p to denote the pair of s ∈ S and p ∈ W, i.e., p restricted to s. The abstract domain O is parameterized by the choices of the abstraction S,⊑ S and the type (e.g., affine, quadratic, cubic, exponential, . . . ) of natural-valued functions used as polynomial coefficients f 0 ,f 1 ,f 2 ,...,f n ∈ F. As an example, [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF][START_REF] Edsger | A Discipline of Programming[END_REF] → ω•(3x+2)+(2x) uses intervals and affine functions respectively.

As for the operators of the abstract domain, we briefly describe only the join operator and the assignment transfer function. We refer to [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] for more details and examples.

The join operator ⊔ O , given two abstract functions o 1 s 1 → p 1 and o 2 s 2 → p 2 , determines the function o s → p, defined on their common domain s s 1 ⊓ S s 2 with value p p 1 ⊔ P p 2 . Specifically, the unification p 1 ⊔ P p 2 of two polynomials p 1 and p 2 is done in ascending powers of ω, joining the coefficients of similar terms (i.e., terms with the same power of ω). The join of two coefficients f 1 and f 2 is provided by f f 1 ⊔ F f 2 and is defined as a natural-valued function (of the same type of f 1 and f 2 ) greater than f 1 and f 2 (on the domain s). Whenever such function does not exist, we force f to equal 0 and we carry 1 to the unification of terms with next higher degree. Intuitively, whenever natural-valued functions are not sufficient, we naturally resort to ordinals. Let us consider the join ω k •f of two terms ω k •f 1 and ω k •f 2 . Forcing f to equal 0 and carrying 1 to the terms with next higher degree is exactly the same as considering f equal to ω:

ω k •f = ω k •ω = ω k+1 •1+ω k •0 = ω k+1 .
To avoid computing infinite increasing chains of abstract functions, to analyze loops we use a widening operator [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF] ▽ O which is similar to the join ⊔ O but defaults to ⊤ P when the abstract function has increased between iterates.

In order to handle assignments, the abstract domain is equipped with an operation to substitute an arithmetic expression for a variable within a function f ∈ F. Given an abstract function o s → p, an assignment is carried out independently on the abstract state s and on the polynomial p. In particular, an assignment on p is performed in ascending powers of ω, possibly carrying 1 to the term with next higher degree. The need for carrying might occur in case of non-deterministic assignments: it is necessary to take into account all possible outcomes of the assignment, possibly using ω as approximation.

Piecewise-Defined Ordinal-Valued Ranking Functions

In the following, we lift the abstract domain O to piecewise-defined ranking functions [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF].

The elements of the abstract domain belong to V P(S ×W). More specifically, an element v ∈ V of the abstract domain has now the form:

v        s 1 → p 1 . . .
s k → p k where the abstract states s 1 ,...,s k ∈ S induce a partition of the space of environments E and p 1 ,...,p k are ranking functions represented as polynomials

ω k •f k +•••+ω 2 •f 2 +ω•f 1 +f 0 whose coefficients f 0 ,f 1 ,f 2 ,...,f n ∈ F are natural-valued functions of the program variables.
The binary operators of the abstract domain rely on a partition unification algorithm that, given two piecewise-defined ranking functions v 1 and v 2 , modifies the partitions on which they are defined into a common refined partition of the space of program environments. For example, in case of partitions determined by intervals with constant bounds, the unification simply introduces new bounds consequently splitting intervals in both partitions. Then, the binary operators are applied piecewise: the piecewise join ⊔ V computes the piecewise-defined natural-valued ranking function greater than v 1 and v 2 using ⊔ O . The piecewise widening ▽ V keeps only the partition of the domain of the first function. In this way, it prevents the number of pieces of an abstract function from growing indefinitely. It also prevents the indefinite growth of the value of an abstract function by using ▽ O .

The unary operators for assignments and tests are also applied piecewise. In particular, assignments are carried out independently on each abstract state and each ranking function. Then, the resulting covering induced by the over-approximated abstract states is refined (joining overlapping pieces) to obtain once again a partition.

The operators of the abstract domain are combined together to compute an abstract ranking function for a program, through backward invariance analysis. The starting point is the constant function equal

int : x1, x2 while ( x1 = 0 ∧ x2 ≥ 0 ) do if ( x1 > 0 ) then if ( ? ) then x1 := x1 -1 x2 := [-∞,∞] else x2 := x2 -1 else / * x1 < 0 * / if ( ? ) then x1 := x1 + 1 else x2 := x2 -1 x1 := [-∞,∞]
Figure 1 Program with no lexicographic ranking function.

int : x, b x := 0, b := 1 [ while ( b > 0 ) do x := x + 1 ] || [ b := 0 ] int : x, b, z1, z2 z1 := [0,+∞], z2 := [0,+∞], x := 0, b := 1 while ( b > 0 ) do if ( z1 ≤ z2 ) then x := x + 1 z1 := [0,+∞] z2 := z2 -1 else b := 0 Figure 2
Concurrent variant (above) and non-deterministic variant (below) of Dijkstra's random number generator [START_REF] Edsger | A Discipline of Programming[END_REF].

to 0 at the program final control point. The ranking function is then propagated backwards towards the program initial control point taking assignments and tests into account using join and widening for loops. As a consequence of the soundness of all abstract operators (see [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF]), we can establish the soundness of the analysis for proving program termination: the program states for which the analysis finds a ranking function are states from which the program indeed terminates.

Implementation. We have incorporated the implementation of the abstract domain O of ordinalvalued ranking functions into our prototype static analyzer [START_REF] Urban | FuncTion[END_REF] based on piecewise-defined ranking functions. The prototype accepts programs written in (a subset of) C. It is written in OCaml and, at the time of writing, the available abstractions for program environments S are based on intervals [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagons [START_REF] Miné | The Octagon Abstract Domain[END_REF] or convex polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF], and the available abstraction for natural-valued functions F is based on affine functions. The operators for the intervals, octagons and convex polyhedra abstract domains are provided by the APRON library [START_REF] Jeannet | Apron: A Library of Numerical Abstract Domains for Static Analysis[END_REF]. The analysis proceeds by structural induction on the program syntax, iterating loops until an abstract fixpoint is reached. In case of nested loops, a fixpoint on the inner loop is computed for each iteration of the outer loop.

◮ Example 1. Let us consider the program in Figure 1. The variables x 1 and x 2 can have any initial integer value, and the program behaves differently depending on whether x 1 is positive or negative. In case x 1 is positive, the program either decrements the value of x 2 or decrements the value of x 1 and resets x 2 to any value. In case x 1 is negative, the program either increments the value of x 1 or decrements the value of x 2 and resets x 1 to any value (possibly positive). The loop exits when x 1 is equal to zero or x 2 is less than zero.

Note that there does not exist a lexicographic affine ranking function for the loop. In fact, the variables x 1 and x 2 can be alternatively reset to any value at each loop iteration: the value of x 2 is reset in the first branch of the first if statement (i.e., if x 1 > 0) while the value of x 1 is reset in the second branch of the first if statement (i.e., if x 1 < 0).

Nonetheless, the program always terminates, regardless of the initial values for x 1 and x 2 , and regardless of the non-deterministic choices taken during execution. Our prototype is able to prove the program terminating in about 10 seconds (with a widening delay of 3 iterations). We automatically infer the following piecewise-defined ranking function (at loop entry):

f (x 1 ,x 2 ) =      ω 2 +ω•(x 2 -1)-4x 1 +9x 2 -2 x 1 < 0 ∧ x 2 > 0 1 x 1 = 0 ∨ x 2 ≤ 0 ω•(x 1 -1)+9x 1 +4x 2 -7 x 1 > 0 ∧ x 2 > 0
Note that, from any state where x 1 < 0 and x 2 = k 2 > 0, whenever the value of x 1 is reset, it is possible to jump to any state where x 2 = k 2 -1. Thus, f must go up to ω 2 (... and beyond!) as it is possible to jump through unbounded non-determinism to states with value of the most precise ranking function equal to an arbitrary ordinal between ω and ω 2 . Finally, note the expressions identified as coefficients of ω: when x 1 < 0, the coefficient of ω is an expression in x 2 (since x 2 guides the progress towards the final states), and when x 1 > 0, the coefficient of ω is an expression in x 1 (because x 1 now rules the progress towards termination). The expressions are automatically inferred by the analysis without requiring assistance from the user. ◭

Conclusion and Future Work

In this paper, we proposed a parameterized abstract domain for proving termination of imperative programs. The domain automatically infers sufficient conditions for program termination, and synthesizes piecewise-defined ordinal-valued ranking functions through backward invariance analysis.

The full version of this short paper has been published in [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF]. Due to space constraints, we refer to [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] for a comparison with related work.

It remains for future work to extend our research to proving termination under fairness constraints and thus proving liveness properties of (sequential and) concurrent programs. However, as shown in the following example, handling ordinals already allows us to take a first step in this direction.

◮ Example 2. Let us consider the concurrent variant of Dijkstra's random number generator [START_REF] Edsger | A Discipline of Programming[END_REF] in Figure 2. The program is terminating under fairness assumptions. Nonetheless, a program transformation can be applied in order to introduce unbounded non-determinism and thus explicitly represent the fair scheduler within the program [START_REF] Francez | Fairness[END_REF]. Once this transformation is carried out, the resulting nondeterministic program (in Figure 2) can be proved terminating by our ordinal-valued ranking functions.

However, more abstractions are to be expected to handle all practical cases.

In fact, our abstract domain is equipped with an approximation and a computational ordering (here not discussed) which respectively do and do not distinguish between ⊥ W and ⊤ W . We refer to[START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF] for further discussion.

The research leading to these results has received funding from the ARTEMIS Joint Undertaking under grant agreement no. 269335 (ARTEMIS project MBAT) (see Article II.9. of the JU Grant Agreement)


Caterina Urban
email: urban@di.ens.fr

Antoine Miné
email: mine@di.ens.fr

A Decision Tree Abstract Domain for Proving Conditional Termination ⋆

We present a new parameterized abstract domain able to refine existing numerical abstract domains with finite disjunctions. The elements of the abstract domain are decision trees where the decision nodes are labeled with linear constraints, and the leaf nodes belong to a numerical abstract domain. The abstract domain is parametric in the choice between the expressivity and the cost of the linear constraints for the decision nodes (e.g., polyhedral or octagonal constraints), and the choice of the abstract domain for the leaf nodes. We describe an instance of this domain based on piecewise-defined ranking functions for the automatic inference of sufficient preconditions for program termination. We have implemented a static analyzer for proving conditional termination of programs written in (a subset of) C and, using experimental evidence, we show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art and is able to analyze programs that are out of the reach of existing methods.

Introduction

Numerical abstract domains are widely used in static program analysis and verification to maintain information about the set of possible values of the program variables along with the possible numerical relationships between them. The most common abstract domains -intervals [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagons [START_REF] Miné | The Octagon Abstract Domain[END_REF] and convex polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF] -maintain this information using convex sets consisting of conjunctions of linear constraints. The convexity of these abstract domains makes the analysis scalable. On the other hand, it might lead to too harsh approximations and imprecisions in the analysis, ultimately yielding false alarms and a failure of the analyzer to prove the desired program property.

The key for an adequate cost versus precision trade-off is the handling of disjunctions arising during the analysis (e.g., from program tests and loops). In practice, numerical abstract domains are usually refined by adding weak forms of disjunctions to increase the expressivity while minimizing the cost of the analysis [13, 18, 20, 29, etc.].

In this paper, we propose a novel parameterized abstract domain for the disjunctive refinement of numerical abstract domains which is particularly well-suited for proving conditional termination of imperative programs.

The elements of the abstract domain are inspired by the space partitioning trees [START_REF] Fuchs | On Visible Surface Generation by a Priori Tree Structures[END_REF] developed in the context of 3D computer graphics and the use of decision trees in program analysis and verification [START_REF] Bertrane | Static Analysis and Verification of Aerospace Software by Abstract Interpretation[END_REF][START_REF] Jeannet | Representing and Approximating Transfer Functions in Abstract Interpretation of Hetereogeneous Datatypes[END_REF]: they are decision trees where the decision nodes are labeled with linear constraints, and the leaf nodes belong to a numerical abstract domain. These decision trees recursively partition the space of possible values of the program variables inducing disjunctions into the numerical abstract domain.

The partitioning is dynamic: during the analysis, partitions (respectively, decision nodes and constraints) are split (respectively, added) by tests, modified by assignments and joined (respectively, removed) when merging control flows. In order to minimize the cost of the analysis, a widening limits the height of the decision trees and the number of maintained disjunctions.

We also emphasize that the partitioning is semantic-based rather than syntacticbased: the linear constraints labeling the decision nodes are automatically inferred by the analysis and do not necessarily appear in the program.

The abstract domain is parametric in the choice between the expressivity and the cost of the linear constraints for the decision nodes (e.g., polyhedral or octagonal constraints), and the choice of the numerical abstract domain for the leaf nodes. As a result of its adaptability, the abstract domain is well-suited to be used for the inference of different program properties, from program invariants to ranking functions. int f (int x, int y, int r) { while 1 ( r > 0 ) { 2 r = r + x; In the following, we describe an instance of this domain based on piecewise-defined ranking functions [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] for the inference of sufficient preconditions for program termination.

Through this instance we propose an approach to termination analysis of imperative programs which is modular, i.e., which allows reasoning on a portion of the code (e.g., a function) at a time -without any knowledge about the complete program -and reusing the analysis result whenever the same function is called.

To illustrate the potential of our approach, let us consider the simple C function in Figure 1: at each loop iteration, the value of r is increased by the value of x and decreased by the value of y. Our abstract domain, parameterized by polyhedral constraints at the decision nodes and affine ranking functions at the leaf nodes and using a widening with thresholds, is able to automatically infer that the program terminates in at most r loop iterations (i.e., in at most 3r + 1 program steps) if x < y (the constraint x < y not appearing in the program).

Our Contribution. In summary, in this paper we make several contributions. First, we propose a parameterized abstract domain for the disjunctive refinement of numerical abstract domains. We show its adaptability to different abstractions, focusing in particular on piecewise-defined ranking functions for proving program conditional termination. Second, we thoroughly discuss the widening operator for ranking functions, which is non trivial and of independent interest. Finally, we evaluate our approach for termination against state-of-the-art implementations [START_REF] Brockschmidt | Better Termination Proving through Cooperation[END_REF][START_REF] Giesl | Automatic Termination Proofs in the Dependency Pair Framework[END_REF][START_REF] Heizmann | Linear Ranking for Linear Lasso Programs[END_REF].

Termination Semantics

We consider a programming language with non-deterministic statements. The operational semantics of a program is described by a transition system Σ, τ , where Σ is the set of program states and the program transition relation τ ⊆ Σ × Σ describes the possible transitions between states during program execution. Let β τ {s ∈ Σ | ∀s ′ ∈ Σ : s, s ′ ∈ τ } denote the set of final states.

The Floyd/Turing traditional method for proving program termination [START_REF] Floyd | Assigning Meanings to Programs[END_REF] consists in inferring ranking functions, namely mappings from program states to elements of a well-ordered set (e.g., O, < , the well-ordered set of ordinals) whose value decreases during program execution.

Intuitively, we can define a ranking function from the states of a program to ordinal numbers in an incremental way: starting from the program final states and retracing the program backwards while counting the maximum number of performed program steps as value of the function. In [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF], this intuition is formalized into a most precise ranking function1 w ∈ Σ ⇀ O that can be expressed as the least fixpoint of the operator φ starting from the totally undefined function ∅:

w lfp ∅ φ φ(v) λs.      0 if s ∈ β τ sup{v(s ′ ) + 1 | s, s ′ ∈ τ } if s ∈ pre(dom(v)) undefined otherwise where v 1 v 2 dom(v 1 ) ⊆ dom(v 2 ) ∧ ∀x ∈ dom(v 1 ) : v 1 (x) ≤ v 2 (x) and pre(X) {s ∈ Σ | ∀s ′ ∈ Σ : s, s ′ ∈ τ ⇒ s ′ ∈ X}.
The domain dom(w) of w is the set of states definitely leading to program termination: any trace starting in a state s ∈ dom(w) must terminate in at most w(s) execution steps, while at least one trace starting in a state s ∈ dom(w) does not terminate.

The most precise ranking function w is sound and complete to prove program termination (see [START_REF] Cousot | An Abstract Interpretation Framework for Termination[END_REF]). However, it is usually not computable. In [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF], we present decidable abstractions of w by means of piecewise-defined ranking functions over natural numbers [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF] and ordinals [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF]. The abstractions refer to the following approximation order (see [START_REF] Cousot | Higher Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection, and PER Analysis[END_REF] for further discussion on approximation and computational orders of an abstract domain):

v 1 ⊑ v 2 dom(v 1 ) ⊇ dom(v 2 ) ∧ ∀x ∈ dom(v 2 ) : v 1 (x) ≤ v 2 (x).
They compute an over-approximation of the value of the function w and an underapproximation of its domain of definition dom(w). In this way, an abstraction provides sufficient preconditions for program termination: if the abstraction is defined on a program state, then all program execution traces branching from that state are terminating.

Piecewise-defined Ranking Functions

We derive new decidable abstractions of w by introducing the abstract domain of constraint-based decision trees T and combining it with the piecewise-defined ranking functions abstractions from [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF].

Let X = {x 1 , . . . , x n } be a finite and totally ordered set of program variables with value in Z. We split the program state space Σ into program control points P and environments E X → Z, which map each program variable to its integer value at a given program control point. No approximation is made on P. On the other hand, each program control point p ∈ P is associated with an element t ∈ T of the abstract domain T. Specifically, t represents an abstraction of the function v ∈ E ⇀ O defined on the environments related to the program control point p:

E ⇀ O, ⊑ γ T ←-T , ⊑ T .
(we postpone the formal definition of γ T to Section 3.2).

We assume we are given as parameter a (possibly infinite) set L of linear constraints over X (e.g., interval [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagonal [START_REF] Miné | The Octagon Abstract Domain[END_REF] or polyhedral [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF] constraints). We also assume we are given an abstraction of partial functions from environments to ordinals by means of a numerical abstract domain for functions F F, ⊑ F [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF], equipped with a bottom element ⊥ F representing the totally undefined function ∅.

r > 0 x ≥ y x ≥ y ⟘ F 3r + 1 1 1
Fig. 2: Example of constraint-based decision tree abstracting a function. The leaves of the tree represent the value of the function for the satisfied constraints on the variables.

The elements of the abstract domain T are disjunctive refinements of those of F (i.e., piecewisedefined functions) in the form of constraint-based decision trees, i.e., decision trees where the decision nodes are labeled by linear constraints in L, and the leaf nodes belong to F. As an example, in Figure 2, the constraint-based decision tree represents the piecewise-defined partial ranking function of the program in Figure 1:

f (x, y, r) =      1 r ≤ 0 3r + 1 r > 0 ∧ x < y undefined r > 0 ∧ x ≥ y
In the following, we first dive into some more details on the functions abstract domain. Then, we give a more formal presentation of our constraint-based decision trees and all abstract operators, including widening to ensure convergence.

Functions Abstract Domain

The functions abstract domain F abstracts a partial ranking function v ∈ E ⇀ O from environments to ordinals by an element f ∈ F which is a function of the program variables, or the element ⊥ F representing potential non-termination, or the element ⊤ F representing the lack of enough information to conclude. In the following, the leaf nodes belonging to F \ {⊥ F , ⊤ F } and {⊥ F , ⊤ F } will be referred to as defined and undefined leaf nodes, respectively.

In order to under-approximate the domain of definition of the most precise ranking function, the concretization function γ F maps all undefined leaf nodes to the totally undefined function ∅:

γ F (⊥ F ) = γ F (⊤ F ) = ∅
In fact, the computational and approximation ordering of the abstract domain respectively do and do not distinguish between ⊥ F and ⊤ F . In particular, the element ⊤ F is produced and used only by the widening operator discussed in the upcoming Section 3.3.

In [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF], we considered instances of the abstract domain F based on affine functions

f (x 1 , . . . , x n ) = m 1 x 1 + • • • + m n x n + q,
where m 1 , . . . , m n , q are constants. In [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] we extended the abstraction to functions over ordinals.

Remark 1. In this paper, we are mainly focusing on instances of T for program termination. However, we emphasize that T is also well-suited to be instantiated with other numerical abstract domains. In fact, analogously to [START_REF] Gurfinkel | BOXES: A Symbolic Abstract Domain of Boxes[END_REF], we can have F {0, 1} and interpret the abstract domain T as the disjunctive refinement of numerical abstract domains such as intervals [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagons [START_REF] Miné | The Octagon Abstract Domain[END_REF] and convex polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF].

We assume that the abstract domain F is equipped with sound binary operators for approximation ordering ⊑ F , join ⊔ F and widening ▽ F , as well as sound transfer functions for assignments ASSIGN F and tests FILTER F . We refer to [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF][START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] for examples.

Constraint-based Decision Trees

The decision tree abstract domain T is parametric in the choice of the abstract domain F and the set of linear constraints L ⊆ {k

1 x 1 + • • • + k n x n ≤ k n+1 | k 1 , . . . , k n , k n+1 ∈ Z}.
As for boolean decision trees where an ordering is imposed on all decision variables, let < L ∈ L × L be a total order on L. As an example, we can define < L to be the lexicographic order on the coefficients k 1 , . . . , k n and constant k n+1 of the linear constraints.

An element t of the abstract domain T belongs to a set T and is either a leaf node LEAF : f , with f an element of F, or a decision node NODE{c} : t 1 ; t 2 , such that c is a linear constraint in L (in the following denoted by t.c) and the left subtree t 1 and the right subtree t 2 (in the following denoted by t.l and t.r, respectively) belong to T . In particular, given a decision tree NODE{c} : t 1 ; t 2 , the linear constraint c is always the smallest constraint appearing in the tree, and the left and right subtrees t 1 and t 2 are either both leaf nodes or both decision nodes labeled with the same linear constraint c ′ (such that c < L c ′ ), i.e., two decision nodes at the same height in the decision tree are always labeled with the same linear constraint. In order to ensure a canonical representation, we also avoid a constraint c and its negation ¬c simultaneously appearing in a constraint-based decision tree (e.g., by keeping only the largest constraint with respect to < L between c and ¬c).

Remark 2. The choice of maintaining the same constraints at the same height in the decision trees is important for the design of the widening operator as explained in the following Section 3.3.

Algorithm 1 : Tree Unification 1: function UNIFICATION(t1,t2) 2: if ISLEAF(t1) ∧ ISLEAF(t2) then 3: return (t1, t2) 4: else if ISLEAF(t1) ∨ (ISNODE(t1) ∧ ISNODE(t2) ∧ t2.c < L t1.c) then 5:
(l1, l2) ← UNIFICATION(t1, t2.l) 6:

(r1, r2) ← UNIFICATION(t1, t2.r) 7:

return (NODE{t2.c} : l1; r1, NODE{t2.c} : l2; r2) 8:

else if ISLEAF(t2) ∨ (ISNODE(t1) ∧ ISNODE(t2) ∧ t1.c < L t2.c) then 9:
(l1, l2) ← UNIFICATION(t1.l, t2) 10:

(r1, r2) ← UNIFICATION(t1.r, t2) 11:

return (NODE{t1.c} : l1; r1, NODE{t1.c} : l2; r2) 12: else 13:

(l1, l2) ← UNIFICATION(t1.l, t2.l) 14:

(r2, r2) ← UNIFICATION(t1.r, t2.r) 15:

return (NODE{t1.c} : l1; r1, NODE{t2.c} : l2; r2)

A constraint-based decision tree t ∈ T , recursively partitions the space of values of the program variables inducing disjunctions into the abstract domain F. Moreover, since two decision nodes at the same height in the decision tree are always labeled with the same linear constraint, they induce the same partition on their left and right subtrees.

Concretization Function. The concretization function γ T depends on the concretization function γ F of the abstract domain F and produces a (partial) ranking function:

γ T (LEAF : f ) = γ F (f ) γ T (NODE{c} : t 1 ; t 2 ) = γ T (t 1 )| c ∪ γ T (t 2 )| ¬c
where v| c is the partial ranking function v ∈ E ⇀ O whose domain dom(v) is restricted to the environments satisfying the constraint c and ∪ joins partial functions with disjoint domains:

(f 1 ∪f 2 )(x) f 1 (x), if x ∈ dom(f 1 ), and (f 1 ∪f 2 )(x) f 2 (x), if x ∈ dom(f 2 ), where dom(f 1 ) ∩ dom(f 2 ) = ∅.
Ordering, Join. The binary operators for the approximation ordering ⊑ T and join ⊔ T of constraint-based decision trees rely on Algorithm 1 for tree unification. Given two decision trees t 1 ∈ T and t 2 ∈ T , the tree unification algorithm finds a common refinement for the trees, possibly adding decision nodes (cf. Lines 5-7 and Lines 9-11). Note that the tree unification does not loose any information. Then, the binary operations are carried out "leaf-wise" on the unified constraint-based decision trees.

Ordering. Given two unified constraint-based decision trees, their approximation ordering is decided by the approximation ordering ⊑ F of the abstract domain F:

(LEAF : f 1 ) ⊑ T (LEAF : f 2 ) = f 1 ⊑ F f 2 (NODE{c} : l 1 ; r 1 ) ⊑ T (NODE{c} : l 2 ; r 2 ) = (l 1 ⊑ T l 2 ) ∧ (r 1 ⊑ T r 2 )
Algorithm 2 : Tree Augment Join. Similarly, given two unified constraint-based decision trees, their join is built using the join operator ⊔ F of the abstract domain F:

(LEAF : f 1 ) ⊔ T (LEAF : f 2 ) = LEAF : (f 1 ⊔ F f 2 ) (NODE{c} : l 1 ; r 1 ) ⊔ T (NODE{c} : l 2 ; r 2 ) = NODE{c} : (l 1 ⊔ T l 2 ); (r 1 ⊔ T r 2 )
Assignments, Tests. The transfer functions for assignments ASSIGN T and tests FILTER T add, modify or delete decision nodes of a constraint-based decision tree. In particular, both operators rely on Algorithm 2 for the extension of a constraint-based decision tree t ∈ T with decision nodes built from linear constraints in C ⊆ L.

Assignments. We recall that the most precise ranking function w defined in Section 2 is a backward semantics. Consequently, we consider backward assignments to a constraintbased decision tree. The transfer function ASSIGN T is described by Algorithm 3. An assignment x := a to a tree t ∈ T is carried out independently on each constraint c ∈ L appearing in t (cf. Line 4): given a constraint c, the primitive ASSIGN L substitutes the expression a for the variable x within the constraint c. Since the modified constraint may not be representable exactly in L, ASSIGN L produces a set of constraints C ⊆ L approximating it. For instance, non-linear assignments can be modeled using standard linearization techniques [START_REF] Bertrane | Static Analysis and Verification of Aerospace Software by Abstract Interpretation[END_REF]. In case C is empty, it means that the constraint c does not exist anymore and the subtrees of t should be joined (cf. Line 5). In case C is an unsatisfiable set of constraints, it means that c is no longer satisfiable and we should keep only the right subtree of t (cf. Line 6). Otherwise, C is a set of constraints that should be substituted to c in t (cf. Lines 8-10). Finally, an assignment to a leaf node is carried out by the operator ASSIGN F of the abstract domain F (cf. Line 2).

Algorithm 4 : Tree Filter Remark 3. Note that Algorithm 3 is general enough to also handle forward assignments, in case the abstract domain T is instantiated with other numerical abstract domains as mentioned in Remark 1. In fact, it is sufficient to modify the primitive ASSIGN L accordingly in order to handle forward assignments.

Example 1. Let us consider the constraint-based decision tree NODE{xy ≤ 0} : (NODE{y ≤ 0} : α; β); (NODE{y ≤ 0} : γ; δ), where greek letters denote leaf nodes. The forward non-invertible assignment y = 3, modifies the constraint xy ≤ 0 to x ≤ 3 and removes the constraint y ≤ 0 which is no longer satisfiable: NODE{x ≤ 3} : β; δ. Instead, the backward non-deterministic assignment y = ? removes y from any constraint appearing in the tree, enforcing the join of the leaf nodes α and β and the leaf nodes γ and δ:

NODE{x ≤ 0} : (α ⊔ T β); (γ ⊔ T δ). ⊓ ⊔
Tests. The transfer function FILTER T for test statements is described by Algorithm 4. First, a test statement c is handled independently on each leaf node (cf. Line 2). The primitive FILTER L approximates c producing a set of constraints C ⊆ L (cf. Line 5).

Then, the constraint-based decision tree t ∈ T is augmented with C (cf. Line 6).

Note that, following an assignment or a test, the decision trees must be sorted and normalized in order to remove possible multiple occurrences of a constraint c and possible occurrences of both a constraint c and its negation ¬c (e.g., by keeping only the largest constraint with respect to < L between c and ¬c): for example, NODE{y ≤ 1} : (NODE{y ≤ 0} : α; β); (NODE{y ≤ 0} : γ; δ) is sorted as NODE{y ≤ 0} : (NODE{y ≤ 1} : α; γ); (NODE{y ≤ 1} : β; δ) and NODE{-y ≤ -1} : (NODE{y ≤ 0} : α; β); (NODE{y ≤ 0} : γ; δ) is normalized as NODE{y ≤ 0} : γ; β.

The soundness of all the abstract operators of T follows immediately from the soundness of the corresponding abstract operators of F.

Widening

The widening operator ▽ T requires a more thorough discussion. The widening is allowed more freedom than the other operators, in the sense that it is temporary allowed to under-approximate the value of the most precise ranking function or over-approximate its domain of definition, or both -in contrast with the approximation order ⊑. This is necessary in order to extrapolate a ranking function over the program states on which it is not yet defined. This is possible because the only requirement of a static analysis is that, when the iteration sequence with widening is stable for the computational order, its limit is a sound abstraction of the program semantics of interest with respect to the approximation order. For this reason, the widening ▽ T consists of many steps that need to be performed in order to guarantee the soundness of the analysis with respect to the most precise ranking function w. In the following, we will go through these steps and we will discuss them in some detail.

As running example, let us consider Figure 3. In Figure 3a we depict a transition system and the value of the most precise ranking function for the well-founded part of the transition relation. In Figure 3b we represent the concretization of a possible abstract analysis iterate. In this case the abstraction both under-approximates the value of the most precise ranking function (on the second state from the left -case B) and overapproximates its domain of definition (including the first and the last state from the left -case A and C, respectively). In case A, the loop causing non-termination is outside the domain of definition of the (unsound) abstract function, while in case C the loop is inside.

Step 1: Check for Case A. The first step that the widening operator ▽ T has to do is to check for cases like case A, where the domain of definition of the most precise ranking function has been over-approximated including a program state from which a non-terminating loop is reachable. In cases like case A, at the next iteration due to the soundness of all the other abstract operators (cf. Section 3.2) the value of the abstract function will become ⊥ F . In order to handle such situations, the widening ▽ T has to look for leaf nodes whose value is now ⊥ F and that previously belonged to a defined subtree (i.e., a subtree with only defined leaf nodes). Then, it has to substitute their value with ⊤ F in order to prevent successive iterates from mistakenly including again the same program states into the abstract function.

Step 2: Domain Widening -Tree Left Unification. At this point, the widening operator ▽ T calls Algorithm 5 for tree unification. Algorithm 5 is a slight modification of Algorithm 1: given two constraint-based decision trees2 the left unification algorithm enforces the refinement of the first tree on the second, possibly removing decision nodes (by joining if ISLEAF(t1) ∧ ISLEAF(t2) then 3:

return (t1, t2) 4: else 5:

if ISLEAF(t1) ∨ (ISNODE(t1) ∧ ISNODE(t2) ∧ t2.c < L t1.c) then 6:

return LEFT-UNIFICATION(t1, t2.l ⊔ T t2.r) 7: else 8:

(l1, l2) ← LEFT-UNIFICATION(t1.l, t2.l) 9:

(r2, r2) ← LEFT-UNIFICATION(t1.r, t2.r) 10:

return (NODE{t1.c} : l1; r1, NODE{t2.c} : l2; r2) subtrees, cf. Line 6) and thus extrapolating the domain of the abstract ranking function over program states on which it is not yet defined. In this way we might loose information but we ensure convergence limiting the size of the constraint-based decision trees. Note that it is important to check for cases like case A before the tree left unification. Otherwise, since leaf nodes whose value is ⊥ F might disappear when joining subtrees, we would not be able to detect them.

Step 3: Check for Case B and C. The third step that the widening operator ▽ T has to do is to check for cases like case B, where the value of the most precise ranking function has been under-approximated, and cases like case C, where its domain of definition has been over-approximated including a non-terminating loop. In cases like B and C, at the next iteration the value of the abstract function will increase. In order to handle such situations, the widening ▽ T has to look for leaf nodes whose value has increased between two iterates and it has to substitute their value with ⊤ F in order to prevent an indefinite growth. Note that the widening is not able to distinguish between an under-approximation of the value of the most precise ranking function (as in case B) and an over-approximation of its domain of definition as in case C.

The following lemma establishes that the widening operator ▽ T always recovers from the inclusion of non-terminating program states into the domain of an abstract ranking function at some iterate X i (i.e., it always recovers from an over-approximation of the domain dom(w) of the most precise ranking function w -cases A and C):

Lemma 1. dom(γ T (X i )) ⊆ dom(w) ⇒ dom(γ T (X i+1 )) ⊂ dom(γ T (X i ))
It follows that the domain of the limit w T of the iteration sequence with widening is a sound under-approximation of the domain of the most precise ranking function w:

Corollary 1. dom(γ T (w T )) ⊆ dom(w)
In addition, the next lemma establishes that, if at some iterate X i the value of the most precise ranking function w is under-approximated (case B), the iteration sequence with widening ▽ T is not stable: It follows that the value of the limit w T of the iteration sequence with widening is a sound over-approximation of the value of the most precise ranking function w:

Lemma 2. ∃s ∈ dom(γ T (X i ))∩dom(w) : w(s) > γ T (X i )(s) ⇒ s ∈ dom(γ T (X i+1 ))
Corollary 2. ∀s ∈ dom(w) ∩ dom(γ T (w T )) : w(s) ≤ γ T (w T )(s)
Step 4: Value Widening. Once the widening operator ▽ T has checked for possible violations of the soundness and the domain of the abstract ranking function has been extrapolated, the last step is devoted to extrapolating the value of the ranking function over the program states on which it was not yet defined. The heuristic that we used in [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF] has proved to be rather effective and justifies our choice to maintain the same linear constraint at the same height in the decision trees. We decided to widen the leaf nodes defined only in the second tree with respect to their adjacent leaf nodes. The rationale being that programs often loop over consecutive values of a variable, we use the information available in adjacent partitions of the domain of the ranking function to infer the shape of the ranking function for the current partitions, i.e., the leaf nodes defined only in the second tree (cf. Figure 4). Since we maintain the same linear constraint at the same height in the decisions tree, the adjacency between leaf nodes is pretty straightforward to define: two leaf nodes in a constraint-based decision tree are adjacent if their paths from the root differ for exactly one constraint satisfaction. Remark 4. In establishing relationships only between adjacent leaf nodes, we are considering a rather naïve heuristic. Another possibility would be establishing relationships between leaf nodes based on the parity of some variable, or based on numerical relationships between variables. It is also possible to improve the widening by introducing thresholds in the left unification (in order to limit the loss of precision). We plan to investigate these possibilities as part of our future work.

Example 2. Let F be the set of affine functions of the program variables (plus ⊥ F and ⊤ F ) [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF]. We consider the widening between 3 t 1 NODE{x ≤ 0} : (LEAF : 1); t ′ 1 and t 2 NODE{x ≤ 0} : (LEAF : 1); t ′ 2 where the decision (sub)trees t ′ 1 and t ′ 2 are: First, the left unification modifies t ′ 2 into: NODE{xy ≤ 0} : (LEAF : 3); (LEAF : 5). Then, the leaf node LEAF : 5, defined only in t ′ 2 , is widened with respect to its adjacent leaf node LEAF : 3. This produces the leaf node LEAF : 2x + 1.

t ′ 1

⊓ ⊔

Since Algorithm 5 limits the height of constraint-based decision trees (cf.

Step 2) and we prevent the indefinite growth of the value of the functions inside the leaf nodes (cf.

Step 3), the iteration sequence with widening is eventually stable after finitely many steps. Its limit w T is a sound abstraction of the most precise ranking function w:

Theorem 1. w ⊑ γ T (w T ).
Proof. Follows by definition of ⊑ from Corollary 1 and Corollary 2.

⊓ ⊔ Remark 5. The reason for the complexity of the widening operator ▽ T is the coexistence of an approximation and a computational order in the termination semantics domain (cf. Section 2) as well as in the abstract domain. We believe that ours is the first widening in the two-order settings. In case the abstract domain T is instantiated with other numerical abstract domains as mentioned in Remark 1, the widening ▽ T becomes straightforward (only the tree left unification and "leaf-wise" widening ▽ F being needed).

Abstract Termination Semantics

The operators of the abstract domain are combined together to compute an abstraction of the most precise ranking function for a program, through backward invariance analysis. The starting point is the constant function equal to 0 at the program final control point. The ranking function is then propagated backwards towards the program initial control point taking assignments and tests into account with join and widening around loops. As a consequence of the soundness of all abstract operators and the soundness (and termination) of the iteration sequence with widening, we can establish the soundness of the analysis for proving program termination: the program states for which the analysis finds a ranking function are states from which the program indeed terminates.

Example 3. Let us consider the following simple C program:

while 1 ( x > 0 ∧ y > 0 ) { 2 x = x -y; } 3
At each loop iteration, the value of x is decreased until it becomes less than or equal to zero. The program always terminates whatever the initial values for x and y are. We analyze this program using our abstract domain of constraint-based decision trees, parameterized with polyhedral [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF] constraints at the decision nodes and affine functions [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF] at the leaf nodes. The starting point is t 3 = LEAF : 0 at the final control point 3. We use a widening delay of two iterations. At the first iteration, at the program control point 1 we obtain the decision tree t Fig. 5: Overview of the experimental evaluation for FuncTion.

Implementation

We have implemented our abstract domain of constraint-based decision trees T into our prototype static analyzer FuncTion4 based on piecewise-defined ranking functions. A preliminary version of FuncTion [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] (without relational partitioning) participated in the 3rd International Competition on Software Verification (SV-COMP 2014), which featured a category for termination of C programs for the first time.

The prototype accepts programs written in a (subset of) C. It is written in OCaml and, at the time of writing, the available abstractions for handling linear constraints in decision trees are based on intervals [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], octagons [START_REF] Miné | The Octagon Abstract Domain[END_REF] and convex polyhedra [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF], and the available abstractions for ranking functions are based on affine functions. The operators from the intervals, octagons and convex polyhedra abstract domains are provided by the APRON library [START_REF] Jeannet | Apron: A Library of Numerical Abstract Domains for Static Analysis[END_REF]. It is also possible to activate the extension to ordinal-valued ranking functions [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] and tune the precision of the analysis by adjusting the widening delay.

The analysis proceeds by structural induction on the program syntax, iterating loops until an abstract fixpoint is reached. In case of nested loops, a fixpoint on the inner loop is computed for each iteration of the outer loop.

Experiments. We have evaluated our prototype implementation against a set of 87 terminating C programs collected from the SV-COMP 2014 termination category and from various publications in the area [1, 6, 9, etc.]. All the experiments were performed on a 1.30GHz Core i5 system with 4GB of RAM and running Ubuntu 12.04.

In Figure 5, we compared FuncTion to its preliminary version [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF]. In particular, we evaluated the expressiveness and efficiency of two instances of our abstract domain of constraint-based decision trees: FuncTion-OCT (which uses octagonal constraints for labeling the decision nodes) and FuncTion-POLY (which uses polyhedral constraints). In the first column we report the total number of programs that each tool was able to prove termination for. In the second to the fourth column, we consider each tool and we report the number of programs that every other tool was able to prove terminating among the programs that the tool was not able to prove termination for. Finally, the last column reports the average running time in seconds for the programs where the tool proved termination. The results match the expectations: FuncTion-OCT is faster than FuncTion-POLY but less precise in seven examples; also, both FuncTion-OCT and FuncTion-POLY are more precise than FuncTion in its preliminary version. Note that, to improve precision, FuncTion [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] avoids trying to infer a ranking function for the non-reachable states Tot FuncTion AProVE [START_REF] Giesl | Automatic Termination Proofs in the Dependency Pair Framework[END_REF] T2 [START_REF] Brockschmidt | Better Termination Proving through Cooperation[END_REF] Ultimate [START_REF] Heizmann | Linear Ranking for Linear Lasso Programs[END_REF] Fig. 6: Overview of the experimental evaluation for termination.

while FuncTion-OCT and FuncTion-POLY do not apply yet this kind of optimizations: for this reason, FuncTion [START_REF] Urban | An Abstract Domain to Infer Ordinal-Valued Ranking Functions[END_REF] was able to prove termination for respectively six and five programs that FuncTion-OCT and FuncTion-POLY were not able to prove terminating. We also compared FuncTion (using all the available abstractions) to some of the other tools that participated to the termination category of SV-COMP 2014: AProVE [START_REF] Giesl | Automatic Termination Proofs in the Dependency Pair Framework[END_REF], T2 [START_REF] Brockschmidt | Better Termination Proving through Cooperation[END_REF], and Ultimate B üchi Automizer [START_REF] Heizmann | Linear Ranking for Linear Lasso Programs[END_REF]. Figure 6 shows an overview of the experimental evaluation when using a time limit of 300 seconds for each example. In the first column we report the total number of programs that each tool was able to prove termination for. In the second to the fifth column, similarly to Figure 5, we consider each tool and we report the number of programs that every other tool was able to prove terminating among the programs that the tool was not able to prove termination for. Finally, the last columns report the average running time in seconds for the programs where the tool proved termination and the number of time outs (i.e., programs for which the analysis took more than 300 seconds). We observe that FuncTion proved termination of 51 of the 87 programs considered, while the other tools get better results. We noticed that the main reason for this is the value widening heuristic (cf. Section 3.3) used by FuncTion. We plan to study these issues further and improve the widening operator as part of our future work. However, we also observe that FuncTion was able to prove termination for eight programs that AProVE and T2 were not able to prove terminating, and for three programs that Ultimate B üchi Automizer was not able to prove termination for. We noticed that all these programs are characterized by the presence of multiple paths with unrelated or conflicting rankings inside loops: these programs are handled in a natural way by the inherent partitioning at the basis of our tool while the other tools must often resort to heuristics or specific workarounds [START_REF] Cook | Ramsey vs. Lexicographic Termination Proving[END_REF].

Related Work

The use of (binary) decision trees (Binary Decision Diagrams, in particular) for verification has been devoted a large body of work, especially in the area of timed-systems and hybrid-system verification [START_REF] Jeannet | Representing and Approximating Transfer Functions in Abstract Interpretation of Hetereogeneous Datatypes[END_REF]. In this paper, we focus on common program analysis applications and, in this sense, our abstract domain is mostly related to the ones presented in [START_REF] Cousot | A Scalable Segmented Decision Tree Abstract Domain[END_REF][START_REF] Gurfinkel | BOXES: A Symbolic Abstract Domain of Boxes[END_REF]: both ours and these abstract domains are a disjunctive refinement of an abstract domain based on decision trees extended with linear constraints. However, the abstract domain proposed in [START_REF] Gurfinkel | BOXES: A Symbolic Abstract Domain of Boxes[END_REF] is designed specifically for the disjunctive refinement of the intervals abstract domain [START_REF] Cousot | Static Determination of Dynamic Properties of Programs[END_REF], while our abstract domain is parameterized by the (possibly relational) abstract domain we want to build the disjunctive refinement for. Moreover, while our abstract domain is based on binary decision trees where we impose the same linear constraint at the same tree level, in [START_REF] Cousot | A Scalable Segmented Decision Tree Abstract Domain[END_REF] the choices at the decision nodes may differ at each node and their number is not bounded a priori.

In general, despite all the available alternatives [3, 13, 18, 20, 21, 29, etc.], it seems to us that in the literature there is no disjunctive abstract domain well-suited for program termination. A first (minor) reason is the fact that most of the existing disjunctive abstract domains are designed specifically for forward analyses while ranking functions are inferred through backward analysis (cf. Section 3.4). However, the main reason is that adapting existing widening operators to ranking functions is not obvious due to the coexistence of an approximation and computational ordering in the termination semantics domain (cf. Section 2 and Section 3.3).

As for related work on termination, we emphasize that our method is able to directly manipulate ranking functions which are dealt with as any other kind of invariants associated to program control points. In this sense, it differs from the majority of the literature based on the indirect use of invariants for synthesizing ranking functions or just proving termination [1, 2, 5, 7, 25, etc.]. Moreover, our approach is at the same time modular (i.e., able to reason on a portion of the code without any knowledge of the complete program) and able to deal with arbitrary control structures (i.e., it is not limited to simple loops as [START_REF] Podelski | A Complete Method for the Synthesis of Linear Ranking Functions[END_REF] or to non nested loops as [START_REF] Bradley | Linear Ranking with Reachability[END_REF]).

Finally, in the literature, we found only few works that have addressed the problem of automatically finding preconditions for program termination. In [START_REF] Cook | Proving Conditional Termination[END_REF], the authors proposed a method based on preconditions generating ranking functions from potential rankings (i.e., mappings to elements of a well-ordered set whose value does not necessarily decrease during program execution), while our preconditions are inherently obtained from the inferred ranking functions as the set of programs state for which the ranking function is defined. Thus, our preconditions are derived by under-approximation of the set of terminating states as opposed to the approaches presented in [START_REF] Ganty | Proving Termination Starting from the End[END_REF][START_REF] Massé | Policy Iteration-based Conditional Termination and Ranking Functions[END_REF] where the preconditions are derived by (complementing an) over-approximation of the non-terminating states.

Conclusion and Future Work

In this paper, we proposed a novel parameterized abstract domain for the disjunctive refinement of numerical abstract domains. We have shown its adaptability to different abstractions, focusing in particular on piecewise-defined ranking functions for automatically proving conditional termination. Our approach to program termination is semantic-based and approximate in a provably sound way. It is able to analyze programs that are out of the reach of state-of-the-art methods.

It remains for future work to improve the widening between ranking functions establishing cleverer relationships between leaf nodes of decision trees and introducing thresholds in order to limit the loss of precision. We also plan to design more abstract domains in order to support non-linear ranking functions (e.g., quadratic, cubic, exponential, . . . ).

A Soundness of the Iteration Sequence with Widening

Let φ T ∈ T → T be the abstract counterpart of φ ∈ (Σ ⇀ O) → (Σ ⇀ O) (that uses the sound abstract operators of T for joins ⊔ T , assignments ASSIGN T and tests FILTER T ) and let T be the abstract counterpart of . The limit w T of the iteration sequence with widening:

X 0 = ⊥ T X i+1 = X i if φ T (X i ) T X i ∧ φ T (X i ) ⊑ T X i X i ▽ T φ T (X i ) otherwise
is a sound over-approximation of the most precise ranking function w:

Theorem 1. w ⊑ γ T (w T )
In order to prove Theorem 1, we need some preliminary results. Lemma 1. dom(γ T (X i )) ⊆ dom(w) ⇒ dom(γ T (X i+1 )) ⊂ dom(γ T (X i ))

Lemma 1 establishes that the widening operator ▽ T always recovers from the inclusion of non-terminating program states into the domain of an abstract ranking function at some iterate X i (i.e., it always recovers from an over-approximation of the domain dom(w) of the most precise ranking function w -cases A and C in Section 3.3).

Proof (of Lemma 1).

In case the iteration sequence with widening reaches an iterate X i such that dom(γ T (X i )) ⊆ dom(w) it means that there exists a program state s ∈ dom(γ T (X i )) belonging to a non-terminating program trace σ (i.e., such that some states are repeated infinitely many times in σ). Without loss of generality we can assume that there is a single program state s ′ repeated infinitely many times in σ and that s ′ is the immediate successor of s in σ. Thus, either s ′ ∈ dom(γ T (X i )) or s ′ ∈ dom(γ T (X i )). In case s ′ ∈ dom(γ T (X i )), by the definition of φ, we have s ∈ dom(φ(γ T (X i ))) and, by the soundness of all abstract operators, we have dom(γ T (φ T (X i ))) ⊆ dom(φ(γ T (X i ))) which implies s ∈ dom(γ T (φ T (X i ))). Therefore, by definition of ▽ T , we conclude that dom(γ T (X i+1 )) ⊂ dom(γ T (X i )). In case s ′ ∈ dom(γ T (X i )), without loss of generality we can assume that s and s ′ coincide. Thus, by the definition of φ and the soundness of all abstract operators we have γ T (X i )(s) < γ T (X i )(s) + 1 = φ(γ T (X i ))(s) ≤ γ T (φ T (X i ))(s). Therefore, by the definition of ▽ T we have that s ∈ dom(γ T (X i+1 )) and we conclude that dom(γ T (X i+1 )) ⊂ dom(γ T (X i )).

⊓ ⊔

It follows that the domain of the limit w T of the iteration sequence with widening is a sound under-approximation of the domain of the most precise ranking function w: Corollary 1. dom(γ T (w T )) ⊆ dom(w)

Proof. Let us assume that dom(γ T (w T )) ⊆ dom(w). Then, by Lemma 1 we have that dom(γ T (w T ▽ T φ T (w T ))) ⊂ dom(γ T (w T )), that is φ T (w T ) ⊑ T w T . Thus w T would not be the limit of the iteration sequence with widening.

⊓ ⊔ Lemma 2. ∃s ∈ dom(γ T (X i ))∩dom(w) : w(s) > γ T (X i )(s) ⇒ s ∈ dom(γ T (X i+1 ))

Lemma 2 establishes that, if at some iterate X i the value of the most precise ranking function w is under-approximated (case B in Section 3.3), the iteration sequence with widening ▽ T is not stable.

Proof (of Lemma 2).

In case the iteration sequence with widening reaches an iterate X i such that ∃s ∈ dom(γ T (X i )) ∩ dom(w) : w(s) > γ T (X i )(s) it means that there exists a program trace σ starting at program state s whose length is greater than γ T (X i )(s). Let s ′ be the successor of the state s on the trace σ. Without loss of generality we can assume that σ is the longest program trace starting from s and that w(s ′ ) ≤ γ T (X i )(s ′ ). Thus, by the definition of φ and the soundness of all abstract operators we have w(s) = φ(w)(s) = w(s ′ ) + 1 ≤ γ T (X i )(s ′ ) + 1 = φ(γ T (X i ))(s) ≤ γ T (φ T (X i ))(s), that is w(s) ≤ γ T (φ T (X i ))(s). Now, since w(s) > γ T (X i )(s) and w(s) ≤ γ T (φ T (X i ))(s), we have γ T (X i )(s) < γ T (φ T (X i ))(s) and by definition of ▽ T we conclude that s ∈ dom(γ T (X i+1 )).

⊓ ⊔

It follows that the value of the limit w T of the iteration sequence with widening is a sound over-approximation of the value of the most precise ranking function w: Corollary 2. ∀s ∈ dom(w) ∩ dom(γ T (w T )) : w(s) ≤ γ T (w T )(s)

Proof. Let us assume that ∃s ∈ dom(w) ∩ dom(γ T (w T )) : w(s) > w T (s). Then, by Lemma 2 we have that s ∈ dom(γ T (w T ▽ T φ T (w T ))), that is φ T (w T ) T w T . Thus w T would not be the limit of the iteration sequence with widening.

⊓ ⊔ Now we are ready to prove Theorem 1:

Proof (of Theorem 1). Follows by definition of ⊑ from Corollary 1 and 2. ⊓ ⊔

Fig. 1 :

 1 Fig. 1: Simple C function. It terminates if x < y.

  Most precise ranking function.

Fig. 3 :

 3 Fig. 3: Example of unsound abstraction (b) of a most precise ranking function (a).

Algorithm 5 :

 5 Tree Left Unification 1: function LEFT-UNIFICATION(t1,t2) 2:

Fig. 4 :

 4 Fig. 4: Example of Value Widening.

NODE{x 2 NODE{x

 2 y ≤ 0} : (LEAF : ⊥ F ); (LEAF : 3) t ′ y ≤ 0} : (NODE{x -2y ≤ 0} : (LEAF : 5); (LEAF : ⊥ F )); (LEAF : 3) 3 Redundant constraints in the decision trees are omitted for conciseness.

1 1 = 1 2 = 1 =

 1121 NODE{x ≤ 0} : (LEAF : 1); (NODE{y ≤ 0} : (LEAF : 1); (LEAF : ⊥ F )) which, taking into account the assignment x = xy, becomes t NODE{xy ≤ 0} : (NODE{y ≤ 0} : (LEAF : 2); (LEAF : ⊥ F )); (LEAF : 2) at the program control point 2. At the third iteration the widening comes into action between the decision trees of Example 2 yielding a fixpoint: t 3 NODE{x ≤ 0} : (LEAF : 1); (NODE{xy ≤ 0} : (NODE{y ≤ 0} : (LEAF : 1); (LEAF : 2x + 1)); (LEAF : 3)) (i.e., the ranking function f 1 (x, y) = 2x + 1) which proves that the program terminates in at most 2x + 1 program steps, whatever the initial values for x and y are. ⊓ ⊔

A ⇀ B is the set of partial maps from a set A to a set B.

Algorithm 5 requires the constraints appearing in the first tree to be a subset of those appearing in the second, which can always be ensured by computing t1▽ T (t1 ⊔ T t2) instead of t1▽ T t2.

http://www.di.ens.fr/ ˜urban/FuncTion.html

Acknowledgements. We are grateful to the developers of AProVE [19], T2 [5], and Ultimate B üchi Automizer [22] for their help with the experiments.

⋆ The research leading to these results has received funding from the ARTEMIS Joint Undertaking under grant agreement no. 269335 (ARTEMIS project MBAT) (see Article II.9. of the JU Grant Agreement)

B Simple Example Analysis

Let us consider the simple C program from Example 3:

At each loop iteration, the value of x is decreased until it becomes less than or equal to zero. The program terminates whatever the initial values for x and y are.

We present the analysis of this toy example with our prototype analyzer. We use our abstract domain of constraint-based decision trees, parameterized with polyhedral [START_REF] Cousot | Automatic Discovery of Linear Restraints Among Variables of a Program[END_REF] constraints at the decision nodes and affine ranking functions [START_REF] Urban | The Abstract Domain of Segmented Ranking Functions[END_REF] at the leaf nodes, and a widening delay of two iterations. The starting point is the constant function equal to zero at the program final control point:

:

LEAF : 0

The ranking function is then propagated backwards towards the program initial control point taking assignments and tests into account with join and widening around loops:

Note that, the transfer functions for assignments ASSIGN T and tests FILTER T increase the value of the ranking function at the leaves in order to "count" the program steps.

:

NODE{x ≤ 0} : (LEAF : 1); (NODE{y ≤ 0} : (LEAF : 1); (LEAF :

After the first iterate the analysis infers that the program terminates in one program step if x ≤ 0 or y ≤ 0 (i.e., if the loop condition is not satisfied).

:

NODE{xy ≤ 0} : (NODE{y ≤ 0} : (LEAF : 2); (LEAF :

At program control point 2, in order to cope with the assignment x = xy, x is replaced with xy in the constraint-based decision tree.

NODE{x ≤ 0} : (LEAF : 1); (NODE{xy ≤ 0} : (NODE{y ≤ 0} : (LEAF : 1); (LEAF :

After the second iterate we know that the program terminates in three step if x ≤ y (i.e., if the while loop is executed only once) and in one step if the while loop is not entered.

After the third iterate we know that the program terminates in five steps if the while loop is executed twice, in three steps if the while loop is executed once, and in one step if the while loop is not entered.

:

NODE{x ≤ 0} : (LEAF : 1); (NODE{xy ≤ 0} : (NODE{y ≤ 0} : (LEAF : 1); (LEAF : 2x + 1)); (LEAF : 3))

The widening infers that the program terminates in 2x + 1 program steps if the while loop is entered and in one step otherwise. { convergence:

At the fourth iteration the analysis with our abstract domain converges: the program terminates in at most 2x + 1 program steps, whatever the initial values for x and y are.