Christophe Roche
email: christophe.roche@univ-savoie.fr

Marie Calberg-Challot
email: marie.calberg-challot@ontologos-corp.com

Luc Damas
email: luc.damas@univ-savoie.fr

Philippe Rouard
email: philippe.rouard@edf.fr

ONTOTERMINOLOGY A New Paradigm for Terminology

Keywords: Ontology, Terminology, Ontoterminology, Knowledge representation, Term definition, Concept definition, Hyper schema

Today, collaboration and the exchange of information are increasing steadily and players need to agree on the meaning of words. The first task is therefore to define the domain's terminology. However, terminology building remains a demanding and time-consuming task, even in specialised domains where standards already exist. While reaching a consensus on the definition of terms written in natural language remains difficult, we have observed that in specialised technical domains, experts agree on the domain conceptualisation when it is defined in a formal language. Based on this observation, we have introduced a new paradigm for terminology called ontoterminology. The main idea is to separate the linguistic dimension from the conceptual dimension of terminology and establish relationships between them. The linguistic component consists of terms (both normalised and non-normalised specialised words) linked by linguistic relationships such as hyponymy and synonymy. The term definition, written in natural-language, is considered a linguistic explanation. The conceptual component is a formal ontology whose concepts are linked by conceptual relationships like the is-a (kind of) and part-of relations. The concept definition, written in a formal language, is viewed as logical specification. An ontoterminology enables us to link these two non-isomorphic networks in a global and coherent system.

INTRODUCTION

Building terminology is a demanding and expensive task. Writing definitions taking into account the different meanings remains difficult, even in technical domains where standards already exist.

We have observed that although experts share the same domain conceptualisation, they do not necessarily agree on the definition of terms when written in natural language -we should bear in mind that from the terminology point of view, a term is a "specialised linguistic unit" which denotes a concept of the domain called the meaning of the term. We have also observed that each time communication problems occur experts refer mainly to technical diagrams or formulas rather than texts or standards. In fact, experts agree on concept definitions when they are written in a formal (logical) or semi-formal (e.g. conceptual graph) language. These definitions are objective since their interpretation is ruled by a formal system.

The main contribution of this article is to claim that in terminology (especially for technical domains), terms i.e. the "verbal definition of a concept" (ISO 1087) need to be separated from concept names since they belong to two different semiotic systems. The first is a linguistic system while the second is conceptual. Similarly, term definitions written in natural language need to be separated from concept definitions written in a formal language. The former are viewed as linguistic explanations while the latter are considered logical specifications of concept. The result is a new kind of terminology called ontoterminology (since the meaning of terms relies on a formal ontology) which brings these two non-isomorphic systems together into a coherent, global one.

ONTOTERMINOLOGY

Separating the linguistic dimension of terminology from its conceptual dimension has led us to introducing a new paradigm for terminology called ontoterminology. This implies that terms should be separated from concepts as well as term definitions from concept definitions.

Although in the General Theory of Terminology the meaning of a term is a concept, the main goal of terminology is not to represent concepts in order to manipulate them (as in artificial intelligence) but to define a common vocabulary we hope is consensual. The concept in terminology does not exist in itself. It exists through the definition of the term written in natural language.

On the other hand, conceptualisation is the central issue in specialised domains. It is built according to a given theory using a formal (or semiformal) language following the epistemological principles of formal language. This means that conceptualisation does not belong to natural language. The logical specification of the concept is identified to the concept itself on which experts agree and to which they refer when ambiguities occur. From this point of view, one could say that the definition of the term paraphrases the formal definition of the concept denoted by the term. The definition of the term written in natural language is then a linguistic explanation of the concept which also describes the linguistic usage of the term.

Conceptualisation is the concern of knowledge engineering. It is for this reason that we claim that ontology [START_REF] Staab | Handbook on Ontologies[END_REF]), (Gomez-Perez et al. 2004), [START_REF] Roche | Ontology: a Survey[END_REF] represents one of the most promising ways forward for terminology. In point of fact, ontology and terminology share the same goal: "An [explicit] ontology may take a variety of forms, but necessarily it will include a vocabulary of terms and some specification of their meaning (i.e. definitions)" [START_REF] Ushold | Ontologies: Principles, Methods and Applications[END_REF]. Nevertheless, we have to bear in mind that an ontology, defined as a "specification of a conceptualisation", is primarily "a description (like a formal specification of a program) of the concepts and relationships that can exist" [START_REF] Gruber | A Translation Approach to Portable Ontology Specifications[END_REF]. Therefore, an ontology is not a terminology. The linguistic dimension of terminology, sometimes confused with the LSP (language for special purpose) lexicon, has to be taken into account. Terms can not be reduced to arbitrary words or labels stuck onto concepts. Terms of usage, normalised terms, lexical forms (including terminological variations and reductions, rhetorical figures like ellipsis, etc.) as well as linguistic relationships are central features in terminology.

Saying is Not Modelling

Terminology relies on two kinds of related but separate systems. The linguistic system is directly linked to specialised speech and text while the conceptual system is the concern of domain modelling. Writing specialised text is different from conceptualisation. Even if one can extract some useful information from text [START_REF] Buitelaar | Ontology Learning from Text: Methods, Evaluation and Applications[END_REF], [START_REF] Daille | Recent Trends in Computational Terminology[END_REF], saying is not modelling [START_REF] Roche | Saying is not modelling[END_REF]. The lexical structure (the network of terms linked by linguistic relationships such as hyponymy or synonymy) is not isomorphic with the conceptual structure (the network of concepts linked by conceptual relationships such as 'a kind of' or 'part of') as illustrated by the following simple example (figures 1 and 2). In fact we need to bear in mind that writing documents is the concern of textual linguistics, one of whose principles is the incompleteness of text. Whereas building ontology, viewed as taskindependent knowledge, is the concern of modelling based on formal (and not natural) languages. We should also bear in mind that using rhetorical figures like ellipsis in writing text modifies the perception of any concepts we may have. In the previous example (figures 1 and 2) the term "voltage relay" does not denote a <Voltage relay> concept which would be a sub-concept of <Relay>. It denotes the <Voltage threshold relay> concept which is a subconcept of <Threshold relay>. Let us notice that the linguistic expression "voltage threshold relay" is not in usage, but can be defined as a normalised term.

Although we can extract some useful information from texts, ontology cannot be built directly from them since we need ontology for understanding text (understanding text requires extra-linguistic knowledge which by definition is not included in the corpus). This is why we have introduced the new paradigm of ontoterminology [START_REF] Roche | Saying is not modelling[END_REF] to take into account these two different activitiesconceptualisation and writing text -and to focus on conceptualisation. The main goal of terminology is first to understand and conceptualise the world and then to name it. Ontoterminology allows building a new kind of terminology in which the concept plays a central role. An ontoterminology is a terminology whose terms, either of usage or normalised, are related to concepts defined in a formal ontology. This makes it possible to manage the linguistic and conceptual dimensions of terminology and provide two kinds of definition: the first formally defines the concept whereas the second explains the term and its usage from a linguistic point of view.

Term and Concept

Concepts in ontoterminology exist in their own right. Thus, ontoterminology manages terms as well as concepts; both are entries in this new kind of terminology. It also means that term and concept definitions are separate but connected since the meaning of a term is related to a concept. In the example below (see figure 3), these definitions appear in two different cards, one for the concept and another for the term.

Ontoterminology enables focusing on the conceptual and linguistic dimensions of terminology. Terms and concepts belong to different and non-isomorphic semiotic systems. In order to show such a difference, terms, as linguistic expressions, are written between quotation marks e.g. "turbine", while concepts, as entities of a formal system, are written between chevrons and start with an upper case e.g. < Hydraulic turbine>.

If ontoterminology enables normalisation of language, unlike classical terminology it also enables preserving the diversity of language between different communities of practice since they share the same domain conceptualisation. In point of fact, two different terms can denote the same concept whose name should be written so that we understand the right place of the concept in the ontology. Such concept names define normalised terms which cannot be used in text (e.g. because they are too long) but are necessary for term meaning and understanding. For example "voltage relay" in English and "relais de tension" in French denote the same concept of <Voltage threshold relay>.

Conceptual Structure

The conceptual relationships are used for structuring entries. In figure 3 the concepts are listed in alphabetical order combined with either the "is-a" or the "part-of" relationship. These conceptual relationships are also used for building the lexical structure which is automatically updated each time the conceptualisation is modified.

Words and linguistic relationships are no longer the only means to access information in terminology. Associating information to concepts, e.g term definitions, documents, returns on experience, etc., amounts to classifying expert knowledge in the terminology.

It is also possible to define new paradigms of navigation based on the domain ontology. Ontology can be viewed as a conceptual map [START_REF] Tricot | Visual Information Exploration: A Return on Experience in Knowledge Base Management[END_REF] in which the experts navigate along the "is-a" and "part-of" relationships in order to access information connected to concepts (figures 3, 4 and 5).

Schemas play a key role in technical domains.

From the conceptual point of view, they represent one of the most important references. Experts agree on this kind of independent natural language knowledge, easier to understand and more consensual than texts. They refer to schemas every time a communication problem occurs or when an explanation is required. A schema describes a physical entity and the parts which make up it. Each of these parts is also described by its own schema. Entities and components are modelled by concepts linked by the part-of relationship. These concepts create a network of part-of linked concepts which allows users to browse from a schema describing the current concept to a more detailed or global schema associated to one of its part-of concepts. Just as hypertext has defined a new method of corpus navigation using textual links, hyper schema defines a new method of knowledge base navigation attached to the domain ontology using conceptual links (see figures 4 and 5).

METHODOLOGY

Unlike textual terminology's semasiological approach which relies essentially on texts for specialised vocabulary extraction [START_REF] Buitelaar | Ontology Learning from Text: Methods, Evaluation and Applications[END_REF], [START_REF] Daille | Recent Trends in Computational Terminology[END_REF], ontoterminology is based on an onomasiological approach. It consists in first defining the domain ontology and then identifying the most suitable terms to denote the concepts (if necessary, new normalised terms are proposed). Our intention is not to compare the two approaches, their goals remain different: the former focuses on specialised vocabulary whereas the latter focuses on conceptualisation. We should just bear in mind that the lexical structure extracted from a corpus does not match the conceptual structure directly defined by experts using a formal language: "saying is not modelling" (Roche 2007) (figures 1 and 2).

Building ontoterminology requires a dedicated methodology from concept to term. Experts play a key role for each step of the Ousia method developed by the University of Savoie and Ontologos corp.

They began by identifying concepts and their relationships. The result is a semiformal conceptual network where the part-of and isa relationships play a central role. This conceptual network is defined using the SNCW tool (Semantic Network Craft Workbench). There are few constraints on the conceptual graph as a semi-formal representation. It remains to formally define concepts in an ontology. This step is performed using the OCW environment (Ontology Craft workbench). OCW is a software for building ontology defined by specific differentiation (see figure 2) [START_REF] Roche | The "specific-difference" principle: a methodology for building consensual and coherent ontologies[END_REF]. The next step is to identify the "specialised linguistic units" -which can be extracted automatically from texts -and to define them in natural language. The final step consists in associating the terms with the concepts previously defined.

VALIDATION

Ontoterminology is currently used in different technical domains. One of them concerns a common vocabulary defined for maintenance applications in hydraulic installations for EDF's CIH group.

The EDF (Electricité de France) Group is a leading player in the European energy industry. It is present in all areas of the electricity value chain, from generation to trading. Leader on the French electricity market, EDF is also solidly implanted in the United Kingdom, Germany and Italy.

The CIH (Centre d'Ingénierie Hydraulique) group is in charge of hydraulic installations. Hydraulic installations are complex structures where many different technical domains have to be taken into account: hydraulic turbines, alternators, transformers, gates, regulation, etc.

One of the first tasks to perform was to define a common dictionary. Each community of practice speaks its own language but has to communicate and exchange information with other communities sharing the same environment and the same domain conceptualisation. Ontoterminology enabled linking the different vocabularies to the same conceptualisation. It then became possible to associate different terms belonging to different communities to the same concept and vice versa, so that the different ways of referring to a given concept were known for each of them. It was also possible to attach information to concepts, such as reference documents (e.g. standards, schemas), returns of experience, expert lists, etc. The result is a software environment which is also used for learning and knowledge capitalisation. Access information relies on the domain ontology and provides new ways of interactive navigation like hyper schemas.

CONCLUSIONS

Experts require terminology which clearly defines terms in relation to the domain conceptualisation. Even if term definitions written in natural language are useful, they are not always consensual unlike domain conceptualisation. Experts also require a terminology which is able to manage and preserve the diversity of language, for instance the capability to use different words to denote the same concept.

We have introduced the paradigm of ontoterminology, a terminology whose conceptual model is a formal ontology, in order to separate the definition of term (viewed as a linguistic explanation) from the definition of concept (considered as a logical specification). This implies that a concept is neither a term nor a definition of a term.

The structure of ontology-oriented terminology relies on the conceptual relationships from which linguistic relationships can be built. Furthermore, with such an approach new navigation methods for browsing the knowledge base attached to the terminology become possible. Ontology can in fact be viewed as a conceptual map in which experts navigate along the "is-a" and "part-of" relationships in order to access to information attached to concepts.

Figure 1 :

 1 Figure 1: The lexical structure of terms.

Figure 2 :

 2 Figure 2: The ontology of relay.

Figure 3 :

 3 Figure 3: The ontoterminology of hydraulic turbines.

Figure 4 :

 4 Figure 4: The conceptual structure of a turbine.

Figure 5 :

 5 Figure 5: A hyper schema.


David Monniaux

Julien Le Guen

Stratified Static Analysis Based on Variable Dependencies *

In static analysis by abstract interpretation, one often uses widening operators in order to enforce convergence within finite time to an inductive invariant. Certain widening operators, including the classical one over finite polyhedra, exhibit an unintuitive behavior: analyzing the program over a subset of its variables may lead a more precise result than analyzing the original program! In this article, we present simple workarounds for such behavior.

Introduction

During experiments, we found examples over which classical polyhedral analysis [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], even with alternative widenings [START_REF] Bagnara | Precise widening operators for convex polyhedra[END_REF], would fail to discover some simple program invariants, which could sometimes even be discovered by interval analysis. This would even happen on simple loops, e.g. for(int i=0; i<N; i++), if the loop contained a nested loop not touching i: the analysis would not discover i ≥ 0! It is counter-intuitive that difficulties in analyzing the behavior of the program on other variables should lead to imprecise results for i.

In some of these examples, such as this simple loop, the lost invariants could be easily recovered by syntactic pattern-matching, but such techniques are brittle. We therefore searched for techniques inspired by our intuition that poor results on certain variables should not impact variables not depending on them.

Generalities and Notations

We consider the strongest invariant of a loop (or, more generally, of a program), defined as the least fixed point lfp Ψ of a monotone operator Ψ over sets of program states [START_REF] Cousot | Abstract interpretation frameworks[END_REF]. For instance, in program 2, the strongest invariant of the loop is the least fixed point in (P(Z × Z), ⊆) of the operator Ψ(X) = {(1, 0)} ∪ {(i + 1,

j + i) | (i, j) ∈ X ∧ i ≤ 5} (1)
Explicit-state model-checking computes such invariants as explicitly represented sets of states (that is, for each state there exists some little data structure). Implicit-state model checking uses compact representations of such sets, such as binary decision diagrams, and computes the least solution of Ψ(X) = X by finding the limit of the ascending sequence X 0 = ∅, X n+1 = Ψ(X n ); for systems with at most n states, this limit is reached within at most n iterations. For infinite state systems such as software programs 1 such an approach is infeasible, because (a) the sets of states X i may be large (or even infinite, if infinite nondeterminism is used) (b) the sequence may not converge within a finite number of iterations.

Abstract interpretation [START_REF] Cousot | Abstract interpretation frameworks[END_REF][START_REF] Cortesi | Widening and narrowing operators for abstract interpretation[END_REF] solves point (a) by replacing arbitrary sets of states by overapproximations; for instance, a set of points in Z n or Q n may be replaced by an enclosing convex polyhedron [START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF][START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]. A given analysis thus restricts itself to a given abstract domain of sets of states; in this article, we focus, as an example, on the domain of polyhedra, but there exist many other abstract domains, for numerical [START_REF] Miné | Domaines numériques abstraits faiblement relationnels[END_REF] or non-numerical states. The operator Ψ on concrete states is replaced by an abstract operator Ψ ♯ , satisfying a soundness condition Ψ(X ♯ ) ⊆ Ψ ♯ (X ♯ ) for all X ♯ . 2 Problem (b), that is, failure for the sequence X ♯ n+1 = Ψ ♯ (X ♯ n ) to become stationary, remains if the abstract domains contains infinite strictly ascending sequences; 3 this is for instance the case of the domain of convex polyhedra. Some form of convergence acceleration is thus needed. Starting with u ♯ 0 = ∅, upwards iterations with widening [START_REF] Cortesi | Widening and narrowing operators for abstract interpretation[END_REF][START_REF] Cousot | Abstract interpretation frameworks[END_REF] compute

4 u ♯ n+1 = u ♯ n ▽(u ♯ n ⊔ Ψ ♯ (u ♯ n )) (2)
x ⊔ y is such that x, y ⊆ x ⊔ y (in the case of polyhedra, ⊔ is generally taken to be the convex hull), and ▽ is a widening operator, such that for all x ⊆ y, y ⊆ x▽y (soundness property), and any sequence of the form u ♯ n+1 = u ♯ n ▽v ♯ n , where v ♯ n is any other sequence, is stationary: after a certain N , it is constant (termination property). Then,

Ψ(u ♯ N ) ⊆ Ψ ♯ (u ♯ N ) ⊆ u ♯ N ▽(u ♯ N ⊔ Ψ ♯ (u ♯ N )) = u ♯ N , thus Ψ(u ♯ N ) ⊆ u ♯ N
, which means that u ♯ N is an inductive invariant of the program, in which the strongest invariant is included.

Once an inductive invariant u ♯ N is obtained, it may be refined by narrowing iterations, which in practice generally consist in computing Ψ ♯ k (u ♯ N ) until the sequence becomes stationary or k exceeds a preset limit.

Widening operators have various unpleasant properties. The best known is that they bring imprecision: the result of widening/narrowing iterations may be strictly larger than the least element of the abstract domain that is an inductive invariant, let alone an invariant (in Sec. 5 we shall list some alternative approaches that do not suffer from this inconvenience, at the expense of generality). The contribution of this article is a generic method to reduce some of the imprecision induced by widening.

Motivating Example

Classical polyhedral analysis [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], 5 when applied to Listing 1, discovers that i ≥ 1 ∧ i ≤ 5 is an invariant at the head of the loop. Yet, running the same analysis on Listing 2 yields i ≤ 5 but not i ≥ 1.

Listing 1: Loop until 5 i n t i = 1 ;

while ( i <=5) { i = i + 1 ; } Listing 2: j = i(i + 1)/2 i n t i =1 , j = 0 ; while ( i <=5) { j = j + i ; i = i + 1 ; } n0 n1 n2 n3 n4 i ← 1 j ← 0 i ≤ 5 j ← j + i i ← i + 1 i > 5
This example is not fortuitous: it models how to address consecutive lines of a matrix in lower triangular packed storage mode. In that memory-effective approach, the matrix is stored in memory as a unidimensional array, each line next to the preceding one, and line number i only uses i positions in the array: j is the index of the start of the line in the array.

2 Some presentations of abstract interpretation distinguish the abstract element X ♯ from the set of states γ(X ♯ ) that it represents. In this article, we chose not to, in order to simplify notations. 3 Again, for practical purposes, it suffices that there exist exceedingly long finite ascending sequences for analysis to become unfeasible. 4 Following the usage in APRON [START_REF] Jeannet | APRON: A library of numerical abstract domains for static analysis[END_REF], our definition of u▽v assumes that u ⊆ v; if this is not the case, use u▽(u ⊔ v) instead. 5 , last line). The table also shows the polyhedra found after two narrowing iterations. The resulting polyhedron, even without narrowing iterations, is much more precise than the one found by classic analysis.

♯ 0 u ♯ 1 u ♯ 2 u ♯ 3 u ♯ 4 u ♯ 5 Classic n1 (
Program 1 is an abstraction of Program 2: each execution of the latter maps to an execution of the former. Yet, the analysis of the former produces a more precise loop invariant than the analysis of the latter. This is an example of the non-monotonicity of analyzes using widenings, a long-known phenomenon [7, ex. 11]: a more precise abstraction may ultimately lead to less precision in the final analysis result.

Analysis of Program 2 with the basic upwards iteration and widening scheme (widening at every iteration) [START_REF] Cousot | Abstract interpretation frameworks[END_REF], using the standard widening on polyhedra,6 yields the successive polyhedra

• i = 1 ∧ j = 0
• -i+j ≥ -1∧i ≥ 1: draw a line through the first two reachable states and obtain a polyhedron in (i, j) generated by vertex (1, 0) and ray (1, 1);

• -i + j ≥ -1 ∧ 7i -4j ≥ 7: polyhedron in (i, j) generated by vertex (1, 0) and rays (1, 1) and (4, 7).

So far, so good: such polyhedra still imply i ≥ 1. At the next iteration, however, this constraint is lost and one gets the polyhedron -i + j ≥ -1, and finally ⊤, the whole plane. The constraint i ≤ 5 is recovered by one step of downwards iteration. Analysis with the improved widening proposed by Bagnara et al. [START_REF] Bagnara | Precise widening operators for convex polyhedra[END_REF], as implemented in the Parma Polyhedra Library, yields a different iteration sequence, but still reaches ⊤ at the end.

If one runs a polyhedral analysis on Program 1, one gets the inductive invariant 1 ≤ i ≤ 5, which is also valid for Program 2. Intersecting this invariant with the output of the widening in the analysis of Program 2 yields a reasonably precise polyhedron (Table 1).

Thus, the basic idea of our method: run preliminary analyzes over abstractions of the program obtained by removing some of the variables, in order to refine the analysis of the complete program. In order to further convey our intuition, let us remark that Prog. 2 is the result of loop fusion over the following program :

f o r ( i = 1 ; i <=5; i ++) t [ i ]= i ; f o r ( i = 1 ; i <=5; i ++) j += t [ i ] ;
Normal forward polyhedral analysis on this program will find good invariants for both loops. In particular, the second loop may not perturb analysis of the first loop. It seems reasonable that the same applies to the code after loop fusion.

The same code could have been the result of the compilation into C of a data-flow program (e.g. Simulink or Lustre) consisting in a ramp generator and an integrator: ramp 1 . . . 5 Σ Again, it seems natural that the analysis of the integrator should not hamper the analysis of the ramp.

Stratified Analysis

We have investigated two approaches. In stratified analysis, we successively perform several static analyzes by abstract interpretation, the results from each analysis being used to refine the following ones. In stratified widening, a single analysis pass is performed, but with a widening improving on and derived from the traditional widening on polyhedra.

Dependency Strata

We consider a set S of subsets of the set of variables V of the program, such that V ∈ S; we order it by inclusion. An immediate predecessor of S ∈ S, denoted by S ′ ≺ S, is S ′ such that S ′ S and there is no S ′′ such that S ′ S ′′ S.

In practice, if we have a relationship v 1 → v 2 meaning "v 1 flows into v 2 through some computation" or "v 2 depends on v 1 ", then the elements of S are, in addition to V itself, subsets S of V closed by: if v ∈ S and v ′ → v, then v ′ ∈ S. One way to construct such subsets is to compute for each variable v the set S(v) = {v ′ | v ′ → v}, and add this set to S unless it is already present. For better efficiency, one computes the strongly connected components of →, and takes S(v) for one v in each component.

Note that → needs not be the semantics dependency relation, which takes into account both data and control dependencies. In intuitive (and imprecise) terms, a variable x is said to be datadependent on a variable y if x is assigned to by an expression where y appears; a variable x is said to be control-dependent on a variable y if x is assigned in a program branch executed or not executed according to the value of y. Collecting all program elements on which a variable depends, through data or control dependencies, is known as slicing [START_REF] Weiser | Program slicing[END_REF]. If → takes into account all dependencies, then S(v) is the slice of variables on which v depends.

A helpful intuition of our method is that it performs analyzes on program slices of increasing size; but this is somewhat misleading, because we do not make any assumption on → and thus it does not necessarily reflect all dependencies. In particular, ignoring control dependencies, compared conventional slicing, may produce simpler slices, of a more manageable size -X. Rival, when developing the Astrée static analyzer, observed that, for many variables, the slice corresponded to approximately 80% of the code, thus slicing did not significantly simplify the program [START_REF] Rival | Understanding the origin of alarms in Astrée[END_REF].

Informal Definition

Let S be a subset of the variables in program P . We note P |S the program P where all references to variables outside S have been replaced by nondet() nondeterministic choices.

Program P i n t i =1 , j = 0 ; while ( i <=5) { j = j + i ; i f ( j % 2 == 0 ) i = i + 1 ; } P |S for S = {i} i n t i = 1 ; while ( i <=5) { i f ( nondet ( ) ) i = i + 1 ; }
For any program P , let C(P ) be its collecting semantics: the set of reachable states of P . In order to simplify notations, for S ⊆ S ′ , we identify sets of states referring to the variables in S with their completion by all values for variables in S ′ \ S. For any S, P |S is a safe abstraction of P : C(P ) ⊆ C(P |S ). More generally, if S ⊆ S ′ , C(P |S ′ ) ⊆ C(P |S ).

For any program P , let A(P ) be the result of static analysis of P . Correctness of the analysis means C(P ) ⊆ A(P ). Let A(P, K) be the result of the static analysis of P where the semantics of P is restricted to states in K: in other words, all states outside of K are removed from the transition relation. For any K ⊇ C(P ), C(P ) ⊆ A(P, K).

For each S ∈ S, we compute the intermediate analysis result R(S) after all R(S ′ ), S ′ ≺ S, have been computed, as follows:

R(S) = A P |S , S ′ ≺S R(S ′ ) (3)
Remark that in this formula, we could have made S ′ to range over all predecessors without changing the result; however, this would have been less efficient. By induction on the length of the ≺-chains, for all S, R(S) ⊇ C(P |S ). At the end, R(V) ⊇ C(P ) is a correct analysis result for the whole program; in fact, any R(S) ⊇ C(P ), so one can stop the analysis at any step, for instance because of a time limit. This is the analysis performed in §1.2, with S = {{i}, {i, j }}.

Formal Definitions and Variants

Let S ∈ S. We assume that the result R(S ′ ) of the analysis for all S ′ ≺ S has already been computed. Let K ♯ = S ′ ≺S R(S ′ ); we assume that lfp Ψ ⊆ R(S ′ ) for all S ′ ≺ S and thus that lfp Ψ ⊆ K ♯ .

The analysis described at Eqn. 3 is defined by the sequence:

u ♯ n+1 = u ♯ n ▽(u ♯ n ⊔ (Ψ ♯ (u ♯ n ∩ K ♯ ) ∩ K ♯ )) (4)
We compute the limit R(S) = u ♯ N of that stationary sequence, and output u ♯ N ∩ K ♯ . Let us note Ψ |A (X) = Ψ(X ∩ A) ∩ A. In other words, Ψ |A is Ψ with everything outside of A being discarded. The following lemma means that we do not change the strongest invariant by throwing out unreachable states in the definition of the semantics, which is intuitive.

Lemma 1. lfp Ψ = lfp Ψ |A for any A ⊇ lfp Ψ.
Proof. lfp Ψ |A is the limit of the ascending sequence defined by X

0 = ∅, X n+1 = Ψ |A (X n ), lfp Ψ that of Y 0 = ∅, Y n+1 = Ψ(Y n ). By induction, for all n, X n = Y n .
Corollary 2. u ♯ N , and thus u ♯ N ∩ K ♯ , includes lfp Ψ, that is, the reachable states.

Proof. Proof Because y ⊆ x▽y and y ⊆ x ⊔ y for all x, y,

Ψ ♯ (u ♯ N ∩ K ♯ ) ∩ K ♯ ⊆ u ♯ N and thus Ψ K ♯ (u ♯ N ) = Ψ(u ♯ N ∩ K ♯ ) ∩ K ♯ ⊆ u ♯ N . Thus, lfp Ψ K ♯ ⊆ u ♯ N .
The result follows from the lemma. We conclude that, by induction over ≺, for all S, lfp Ψ ⊆ R(S).

We shall now describe a subtly different iteration scheme, which supposes some additional properties of ▽: Definition 3. We say that ▽ satisfies the "up to" termination condition if for any fixed K ♯ , any

u ♯ 0 ⊆ K ♯ , any sequence v ♯ n ⊆ K ♯ the sequence defined by u ♯ n+1 = (u ♯ n ▽v ♯ n ) ∩ K ♯ is stationary if u ♯ n ⊆ v ♯
n for all n. This property ensures the correctness of widening "up to" [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF], a well-known improvement to widening, and is true of the standard widening on polyhedra as well as Bagnara et al.'s improved widening [2, p. 53]. Using the same notations and hypotheses as above, we use this iteration:

u ♯ n+1 = (u ♯ n ▽(u ♯ n ⊔ (Ψ ♯ (u ♯ n ) ∩ K ♯ ))) ∩ K ♯ (5)
Again, once we get a stationary value u ♯ N in this sequence, then it is such that lfp Ψ ⊆ u ♯ N :

Lemma 4. If u ♯ N +1 ⊆ u ♯ N in Eqn. 5, u ♯ N includes lfp Ψ, the set of reachable states. Proof. Proof Ψ(u ♯ N ) ∩ K ♯ ⊆ Ψ ♯ (u ♯ N ) ∩ K ♯ ⊆ u ♯ N +1 ⊆ u ♯ N , from the correctness of Ψ ♯ . Furthermore, by construction, u ♯ N ⊆ K ♯ , thus Ψ(u ♯ N ) ∩ K ♯ = Ψ |K ♯ (u ♯ N ). Ψ |K ♯ (u ♯ N ) ⊆ u ♯ N , thus lfp Ψ |K ♯ ⊆ u ♯ N .
The result follows from Lem. 1.

Stratified Widenings

An alternative to the method described in the preceding section, which runs successive analyzes of increasing precision, is to run a single analysis over a reduced product [START_REF] Cortesi | Widening and narrowing operators for abstract interpretation[END_REF] of polyhedral domains, but with a special widening operator. We shall provide two options for that operator.

Widening with or without Reduction

We distinguish the internal state (P S ) S∈S of the iteration sequence from the set of states represented, as in [START_REF] Monniaux | A minimalistic look at widening operators[END_REF]. The various abstract operations will therefore continue operating on polyhedra as usual: only the widening operator is replaced.

Our widening operators will take a tuple (P S ) S∈S as a first argument and single polyhedron Q as a second argument. A tuple (P S ) S∈S represents the polyhedron

γ ((P S ) S∈S ) = S∈S P S ; (6)
the tuples are ordered point-wise, (P S ) S∈S ⊑ (Q S ) S∈S if and only if for all S, (P S ) ⊆ (Q S ). We note π S (P ) the projection of polyhedron P onto the variables in S. If S ⊆ S ′ , a polyhedron on the variables in S shall be also considered as a polyhedron on the variables in S ′ by keeping the same constraints. This means, in particular, that P ⊆ π S (P ) for any P and S.

The first widening operator is very simple:

(P S ) S∈S ▽ 1 Q = (P S ▽π S (Q)) S∈S ( 7
)
where ▽ is any widening on polyhedra. This widening converges because each coordinate converges, since ▽ is a widening. It is obvious that, if (P S ) S∈S is the resulting limit, then γ ((P S ) S∈S ) is an inductive invariant.

The second widening applies internal reductions. (R S ) S∈S denotes (P S ) S∈S ▽ 2 (Q S ) S∈S . We compute the R S in ascending order with respect to ≺, with the convention that the intersection of zero polyhedra is the full polyhedron:

R S = (P S ▽π S (Q)) ∩ S ′ ≺S R S ′ (8)
Theorem 5. Assuming that ▽ is a widening satisfying the "up to" termination condition (Def. 3), ▽ 2 is a widening.

Proof. Proof Let u (n+1) = u (n) ▽ 2 v (n) be a sequence, with u (n) ⊑ v (n) for all n; each element u (n) consists in u (n)
S for S ∈ S. We prove that for all S ∈ S the sequence u

(n)
S is stationary, by induction over ≺.

For S with no predecessor, (u

(n) S ) is of the form u (n+1) S = u (n) S ▽v (n)
S , and the result follows from ▽ being a widening.

Consider now the property satisfied for all S ′ ≺ S. For all S ′ ≺ S, (u

(n) S ′
) is stationary; thus there is a N such that for n ≥ N , all (u

(n) S ′ ) for S ′ ≺ S are constant. S ′ ≺S u (n)
S ′ is thus constant for n ≥ N . The results follows from ▽ being a widening satisfying our additional property.

Instead of polyhedra, one may use other abstract domains fitted with an operation ⊓ such that a ∩ b ⊆ a ⊓ b for all a, b. Let us however note that ▽ 1 and ▽ 2 yield the same results as the ordinary widening ▽ if applied to domains, such as difference bound matrices or octagons [START_REF] Miné | Domaines numériques abstraits faiblement relationnels[END_REF] where ▽ and projection commute: π S (P )▽π S (Q) = π S (P ▽Q), and therefore that they bring no improvement for such domains: the P S are just projections of P V . More precisely: Lemma 6. Assume that π S (P )▽π S (Q) = π S (P ▽Q) for all P and Q. Any iteration sequence of the form P (n+1) = P (n) ▽Q (n) then satisfies, for all n and S ∈ S, P

(n) S = π S (P (n)
V ), assuming this equality holds for n = 0.

Proof. Proof Regarding ▽ 1 : by induction over n, for any S, P

(n+1) S = P (n) S ▽π S (Q (n) ) = π S (P (n) V )▽π S (Q) = π S (P (n) V ▽Q) = π S (P (n+1) V
). Regarding ▽ 2 : by induction over n, then by induction over S with respect to ≻: (P

(n) S ▽π S (Q (n) ))∩ S ′ ≺S P (n+1) S ′ = (π S (P (n) V )▽π S (Q (n) ))∩ S ′ ≺S π s ′ (P (n+1) V ) = π S (P (n) V ▽π S (Q (n) ))∩ S ′ ≺S π s ′ (P (n+1) V ) = π S (P (n+1) V ) ∩ S ′ ≺S π s ′ (P (n+1) V ) = π S (P (n+1) V
), since for any X and S ′ ≻ S, π S ′ (X) ∩ π S (X) = π S (X).

Generalized Reduction Leads to Nontermination

Communicating information between several abstract domains used at the same time is sometimes referred to as a closure or reduction operation. Our ▽ 2 operation includes a partial closure, with information flowing from a to b if a ≺ b, but not the reverse. One could wonder about applying reductions in all directions. Unfortunately, we would lose the termination property of widening, as demonstrated by the following example. 7Listing 3: Alternating increments i n t i =0 , j = 0 ; while ( t r u e ) { i f ( i <= j ) i ++; e l s e j ++; } i j This loop has different behaviors on odd and even iterations: at iteration 2n, i = n and j = n; at iteration 2n + 1, i = n + 1 and j = n. The results of a static analysis with polyhedra on (i, j), and unions instead of widenings, are, in constraint form: P ♯ 2n : P ♯ ∧ i ≤ n and P ♯ 2n+1 : P ♯ ∧ j ≤ n, P ♯ denoting i ≥ j ∧ i ≤ j + 1 ∧ j ≥ 0 (we identify P ♯ with the conjunctions of the constraints that define it). If for the iteration n = 4 we use widening, 8 we instead obtain P ♯ 4 = P ♯ , which is an inductive invariant.

We have established that this program poses no challenge to "classical" polyhedral analysis. The same is true if we apply one of the analyzes of Sec. 2 or one of the widenings of Sec. Instead of the definition given at Eq. 8, we instead initialize all R S to P S ▽π S (Q), then apply some replacements, or reductions, of the form:

R S := R S ∩ S ′ =S π S (R S ′ ) (9)
If we reach a fixed point for this replacement system, using the terminology from octagons [START_REF] Miné | Domaines numériques abstraits faiblement relationnels[END_REF],

we say that we have applied the closure operation.

Let us first remark that γ ((R S ) S∈S ) is left unchanged any number of such reductions:

Lemma 7. Let (R ′ S ) S∈S be the same as (R S ) S∈S except that R ′ S0 = R S0 ∩ S ′ =S0 π S0 (R S ′ ). Then, γ ((R ′ S ) S∈S ) = γ ((R S ) S∈S ). Proof. Proof γ ((R ′ S ) S∈S ) = S∈S R ′ S = γ ((R S ) S∈S )∩ S ′ =S0 π S0 (R S ′ ) = γ ((R S ) S∈S )∩ S ′ ∈S π S (R S ′ ). Since R S ′ ⊆ π S0 (R S ′ ) for any S ′ , S ′ ∈S π S (R S ′ ) ⊇ S ′ ∈S R S ′ = γ ((R ′ S ) S∈S ).
The result follows.

Because γ ((R S ) S∈S ) does not change, after the reductions, γ ((R S ) S∈S ) is still the same as γ(P ▽Q). Our new "widening" thus verifies the soundness property (see Sec. 2.3); the problem is that it does not verify the termination property! Let us have S = {{i}, {j}, {i, j}}; instead of P {i} , P {j} and P {i,j} we shall respectively note I ♯ , J ♯ and P ♯ . At iteration n, we shall therefore have a polyhedron I ♯ n on {i} (thus, an interval) and one polyhedron J ♯ n on {j} in addition to the polyhedron P ♯ n on {i, j}. If using unions instead of widenings, we have

I ♯ 2n = [0, n], I ♯ 2n+1 = [0, n + 1], J ♯ 2n = [0, n] and J ♯ 2n+1 = [0, n].
Consider now using widening at the iteration n = 4.

I ♯ 4 = I ♯ 3 = [0, 2], but J ♯ 4 = [0, +∞).
Let us now apply the closure operation: we replace P ♯ 4 = P ♯ by its intersection with I ♯ 4 and obtain P ♯ ∧ i ≤ 2; then we replace J ♯ 4 by its intersection with the updated P ♯ 4 and obtain [0, 2]. At the next iteration, with the roles of I ♯ and J ♯ reversed, we obtain I ♯ 5 = [0, 3], J ♯ 5 = [0, 2] after closure, and then

I ♯ 6 = [0, 3], J ♯ 6 = [0, 3]
. The iterations with widening followed by closure behave, on I ♯ and J ♯ , like those with unions -and they do not converge within finite time. Observe that this happens because we alternatively reduce I ♯ → P ♯ → J ♯ and J ♯ → P ♯ → I ♯ , whereas the definitions of Sec. 3.1 only allow I ♯ → P ♯ and J ♯ → P ♯ .

Experimental Results

The stratified analysis presented in section 2, in both variants (Eqn. 4 and Eqn. 5), was evaluated against the classical analysis described by Eqn. 2 on a set of benchmarks used by STMicroelectronics in the development cycle of its compilers, in addition to a few specific examples such as the one from Sec. 1.2.

LAO Kernels is a set of benchmarks internally used for the evaluation of compilers code generators and optimizations. It is mainly composed of small computational kernels representative of the target applications of STMicroelectronics (audio and video stream processing, embedded device control), associated with a testing harness to be able to run them on the target processor. It contains 63 functions, of which 49 contain at least one loop. Loops have to exhibit some properties, like a non-linear relation between variables in the loop scope, in order to benefit from this method. Stratified analysis finds a more precise invariant for 5 of these functions.

Among these 5 functions, discrete cosine transform has three nested loops. The intuition of why stratified analysis performs better is it obtains an invariant for the indices affected by the outer loop before attempting to analyze the inner loop, thus preventing imprecisions during the inner loop analysis to affect the invariant on the outer loop indices.

The dependency relation used to create the strata is based on a modified dataflow graph; strongly connected components (SCC) are reduced to super-nodes, while keeping the existing dependency relations. Initial strata stem from the root nodes of this SCC dependency graph, additional ones are created by following the dependency relations until one stratum encompasses all variables in the dependency graph. In the while loop of the listing 2, the variable j depends from i; the SCC nodes simply consist of {i} and {j}, and the analysis creates two strata {i} and {i, j}.

The two variants of stratified analysis described by Eqn. 4 and Eqn. 5 find the same results, and in all cases find invariants equal to or stronger than those obtained by the classical analysis. Bagnara et al.'s alternate widening [START_REF] Bagnara | Precise widening operators for convex polyhedra[END_REF] yields iteration sequences different from those obtained by the classical widening, but ultimately finds the same invariant; thus, our approach improves on theirs on this benchmark set.

Table 2 shows the number of variables in the outermost stratum, along with the number of strata considered by the analysis and its overhead with respect to the standard analysis using only the classic widening. Some programs exhibit a large number of strata, impacting the cost of the analysis. It is possible to run the expensive stratified analysis after a first cheaper standard analysis, while focusing on certain loop nests (those reaching ⊤ for instance).

We rely on the APRON numerical abstract domain library 9 [14] for all abstract domain computations. APRON implements, among other domains, convex polyhedra with the classical widening, Table 2: Number of variable in the last stratum, number of strata and overhead of stratified analysis for programs that benefit from this method. The baseline for overhead measures is the classic analysis using bare widenings, without delay or widening-up-to).

with linearization of nonlinear expressions following Miné's approach [START_REF] Miné | Symbolic methods to enhance the precision of numerical abstract domains[END_REF]. In addition, in order to compare with Bagnara et al.'s alternate widening, we used the Parma Polyhedra Library10 [1] (with the classical widening, the PPL produces exactly the same results as APRON up to equivalence of constraints, thus providing a means to test for possible bugs in the polyhedral computations).

Related Work

It has long been recognized that analysis using polyhedra over all variables in a program, or even all variables in a single function, is unfeasible because of the high complexity of polyhedral operations in higher dimensions. This is also true of weaker domains such as octagons. For this reason, the Astrée analyzer uses relational domains only on "packs" of variables [START_REF] Blanchet | Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software[END_REF][START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]: for instance, if we have four variables a, b, c, d and two packs {a, b} and {b, c, d}, the analysis will track relationships between a, b and b, c, d separately: no direct relation will be established between a and d.

A related approach is factoring of polyhedra [START_REF] Halbwachs | Some ways to reduce the space dimension in polyhedra computations[END_REF]: when a polyhedron P is a Cartesian product P 1 × . . . × P n of polyhedra in lower dimension, with respectively v i vertices (or, more generally, generators), it is often advantageous to keep this product representation as much as possible instead of considering it as a polyhedron of i v i vertices, because of algorithms that need to work on the generator representation. An alternative is to dispense totally with the generator representation [START_REF] Simon | Exploiting sparsity in polyhedral analysis[END_REF][START_REF] Simon | Simple and precise widenings for H-polyhedra[END_REF].

The literature on slicing is abundant, since the early 1980s [START_REF] Weiser | Program slicing[END_REF]. Syntactic slicing extracts all program statements, variables etc. that affect the value of variable v, or, rather, a safe superset thereof. The resulting slice is executable, which is interesting for testing or debugging methods, but less so for abstract interpretation; this is why we may use lax dependency relations (Sec. 2.1), since we in effect replace any unknown dependency by nondeterministic choice. Semantic slicing relaxes the requirement that the resulting program be a syntactic subset of the original program [START_REF] Ward | Slicing as a program transformation[END_REF]. X. Rival considers a form of abstract semantic slicing [START_REF] Rival | Understanding the origin of alarms in Astrée[END_REF][START_REF] Rival | Traces Abstraction in Static Analysis and Program Transformation[END_REF], where program executions are restricted to those affecting the reachability of undesirable program states (alarms); in contrast, our method does not suppose we have a set of properties (absence of alarms) to prove.

The design of widening operators is surprisingly difficult. The original widening operator on polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] was sensitive to syntax: different ways of representing the same polyhedron in constraint form yielded different widened polyhedra; this problem was later fixed [START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF]. Because the result of iterations with widening is non-monotonic, precision is highly heuristic: in particular, replacing a widening operator by one producing smaller polyhedra at each iteration does not necessarily translate in a smaller invariant in the end [2, p. 42].

Despite this caveat, many widening operators have been proposed for convex polyhedra [2, p. 30] [START_REF] Simon | Simple and precise widenings for H-polyhedra[END_REF]. Many are variants on the classical widening: some apply union in lieu of the classical widening in a way that does not preclude termination [START_REF] Bagnara | Precise widening operators for convex polyhedra[END_REF]; the "up to" widening, also known as widening with thresholds or limited widening [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF], extracts possibly relevant constraints from the program and keeps in P ▽Q the constraints from that set satisfied by both P and Q; a related idea is widening with landmarks, which uses estimates of the number of supplementary iterations necessary to enable a currently disabled transition [START_REF] Simon | Widening polyhedra with landmarks[END_REF]; widening with a care set uses a proof goal and counterexamples in order to guide the widening [START_REF] Wang | Using counterexamples for improving the precision of reachability computation with polyhedra[END_REF]. Our approach is largely orthogonal to these, and in fact can be combined with them.

In the recent years, there has been much interest in techniques for inferring invariants without doing conventional Kleene iterations. Policy iteration (also called strategy iteration; the technique is inspired by game theory) exists in two flavors. Descending policy iteration [START_REF] Gaubert | Static analysis by policy iteration on relational domains[END_REF] solves a descending sequence of least fixed points of simpler operators; these least fixed points may be solved approximately using widenings, thus this technique is orthogonal to ours. In contrast, ascending policy iteration [START_REF] Gawlitza | Precise fixpoint computation through strategy iteration[END_REF] and other techniques based on constraint programming [START_REF] Sankaranarayanan | Mathematical Analysis of Programs[END_REF] or quantifier elimination [START_REF] Monniaux | Automatic modular abstractions for template numerical constraints[END_REF] provide some optimality guarantees, but impose restrictions on the kind of program instructions supported. Such restrictions may be lifted by abstracting program operations into the supported subset [START_REF] Miné | Domaines numériques abstraits faiblement relationnels[END_REF], which may in turn entail an outer loop with widenings.

We finally note that nothing in our approach is specific to polyhedra, or even to numerical domains.

Conclusion

Following our intuition that failure to analyze well parts of a program should not negatively influence precision on other parts not depending on them, we proposed four analysis schemes: two proceed by analyzes of restrictions of the program code to variable subsets, the other ones use alternative widening operators. Though we focused on improving the classical polyhedral analysis, two of our methods apply to any abstract domain, and the two other ones make a reasonable assumption on the underlying abstract domain and its widening operator.

Table 1 :

 1 Comparison of classic static analysis (upward iterations with widening ▽ followed by descending iterations) and stratified static analysis on Program 2. Classic analysis loses the constraint i ≥ 1 and finds ⊤ in 5 iterations. The upper bound i ≤ 5 is found with one narrowing iteration. Stratified analysis on the stratum consisting of variable i first finds 1 ≤ i ≤ 5. Then, it analyzes stratum i, j and intersect with result of stratum i. A fixed point is found after 4 iterations (u ♯ 3

  3.1. Let us now see what happens if we modify the ▽ 2 operator of Sec. 3.1 by allowing reductions not following ≺.

The standard widening on polyhedra P 1 ▽ S P 2 , in intuitive terms, suppresses from P 2 constraints not present in P 1 . In reality, its correct definition contains subtleties regarding polyhedra of dimension less than the dimension of the space, and the original definition[START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] had to be corrected[START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF].[START_REF] Bagnara | Precise widening operators for convex polyhedra[END_REF] recalls the corrected definition.

The fact that widenings followed by reductions with cycles (reduce a using b, then reduce b using a) may not ensure termination is already known. For instance, closure in difference-bound matrices and octagons breaks termination.[16, example 3.7.3, p.

85]8 Applying unions at n first iterations and then applying widening is a standard technique known as delayed widening.

http://apron.cri.ensmp.fr/library/

http://www.cs.unipr.it/ppl/

* This work was partially supported by ANR project "ASOPT † CNRS / VERIMAG; VERIMAG is a joint laboratory of CNRS and Université Joseph Fourier