Marius Bozga
email: fbozga@imag.fr

Radu Iosif
email: iosif@imag.fr

Yassine Lakhnech
email: lakhnechg@imag.fr

On Logics of Aliasing

In this paper we investigate the existence of a deductive veri cation method based on a logic that describes pointer aliasing. The main idea of such a method is that the user has to annotate the program with loop invariants, pre-and post-conditions. The annotations are then automatically checked for validity by propagating weakest preconditions and verifying a number of induced implications. Such a method requires an underlying logic which is decidable and has a sound and complete weakest precondition calculus. We start by presenting a powerful logic (wAL) which can describe the shapes of most recursively de ned data structures (lists, trees, etc.) has a complete weakest precondition calculus but is undecidable. Next, we identify a decidable subset (pAL) for which we show closure under the weakest precondition operators. In the latter logic one loses the ability of describing unbounded heap structures, yet bounded structures can be characterized up to isomorphism. For this logic two sound and complete proof systems are given, one based on natural deduction, and another based on the e ective method of analytic tableaux. The two logics presented in this paper can be seen as extreme values in a framework which attempts to reconcile the naturally oposite goals of expressiveness and decidability.

Introduction

The problem of pointer aliasing plays an important role in the elds of static analysis and software model checking. In general, static analyses used in optimizing compilers check basic properties such as data sharing and circularities in the heap of a program, while model checking deals with the evolution of heap structures, in both shape and contents, over time. An early result 21] shows that precise may-alias analysis in the presence of loops is undecidable. As a consequence, the approach adopted by the static analysis community, is the abstraction-based shape analysis 23]. This method is e ective in the presence of loops, since the domain of the analysis is bounded, but often imprecise. In this paper we present an orthogonal solution to the aliasing problem, in that precision is the primary goal. To ensure termination, we use Floyd's method 10] of annotating the program with pre-, post-conditions and loop invariants. The annotations are subsequently veri ed by a push-button procedure, that computes weakest preconditions expressed using an e ectively decidable logic.

The key is to nd a logic that can altogether (i) express aliasing and shape properties of the program heap, (ii) is e ectively decidable, and moreover, (iii) has a sound and complete weakest precondition calculus with respect to the atomic statements. While the second and third requirements are clear, the rst one is still ambiguous: what kind of speci cations can we express in a decidable heap logic with weakest preconditions? The contribution of this paper is the de nition of a formal framework in which we prove that such logics can be found. Our focus is on imperative programs with destructive updating, in which heaps are viewed as shape graphs with labels only on edges i.e., we ignore from the start the internal states of the objects.

As a starting point, we present a general logic Weak Alias Logic (wAL) that is expressive enough to describe the recursive data structures of interest (lists, trees, dags etc.) as in nite classes of nite graphs. This logic has also a sound and complete weakest precondition calculus with respect to atomic statements such as new object creation and assignment of pointers. The satis ability problem of the wAL logic is found to be undecidable but recursively enumerable, which motivates further searches for semi-decision procedures and non-trivial decidable subsets.

In the rest of the paper, we de ne a decidable subset of wAL, called Propositional Alias Logic (pAL) for describing pointer aliasing that is, moreover, able to characterize arbitrary nite structures and nite classes of structures. The tradeo in de ning pAL is losing the ability to describe a number of interesting shape properties such as listness, (non)circularity, etc. For this logic, we give a proof-theoretic system based on natural deduction, and an e ective tableau decision method. Both systems are shown to be sound and complete. Moreover, the satis ability problem for pAL is shown to be NP-complete. The last point concerns the de nition, in pAL, of weakest preconditions for imperative programs with destructive updating. At this point, we use the wAL weakest precondition calculus, previously developped in 2]. Our weakest precondition calculus for pAL is sound and complete, as a consequence of the soundness and completness of the de nitions for wAL weakest preconditions. Related Work To describe properties of dynamic program stores, various formalisms have been proposed in the literature e.g., L r 1], BI (Bunched Implications) 13], Separation Logic 22] and PAL (Pointer Assertion Language) 17]. As a common point with our work, L r 1] uses regular expressions to describe reachability between two points in the heap and is shown to be decidable, yet the weakest precondition calculus is not developed. On the other hand, BI 13] and Separation Logic 22] produce remarkably simple preconditions and have quite clean proof-theoretic models 18]. Another feature of these formalisms is that they allow for compositional reasoning 19]. As a downside, the quanti er fragment, essential to express weakest preconditions, is undecidable 5], while the ground (propositional) fragment is decidable, a tableau procedure being proposed in 11]. In a later publication 6], a specialization of the ground fragment of BI to tree models is used as a type system for a language, based on -calculus, that handles trees. An e ectively decidable formalism is PAL 17], an extension of second-order monadic logic on trees that allows to describe a restricted class of graphs, known as \graph types" 16], as opposed to our approach that deals with unrestricted graphs. Programs that manipulate such graphs are restricted to updating only the underlying tree (backbone). The resulting actions can thus be described in monadic second-order logic, and the validity of Hoare triples expressed in PAL can be automatically decided 15].

The decision procedures for both L r and PAL use Rabin's result on the monadic second order theory of n successors (SnS) 20]. The decision procedure for the satis ability of SnS is however non-elementary. We show that the decision problem for the pAL logic is NP-complete, thus drastically improving the complexity bounds. Also, to the best of our knowledge, no previously published work on the veri cation of heap properties has the ability to deal with unrestricted (destructively updated) data structures, developing a sound and complete weakest precondition calculus on top of a decidable logic for graphs.

Weak Alias Logic

In this section we introduce Weak Alias Logic (wAL), a logic that is expressive enough for de ning recursive data structures (lists, trees, etc) as in nite classes of nite graphs, as well as for de ning a weakest precondition calculus of imperative programming languages with destructive updating 2]. This section de nes the logic, and Section 5 brie y recalls the weakest precondition calculus that has been developed on top of it.

Before giving the syntax of wAL, let us introduce the notion of heap, which is central in de ning interpretations of wAL formulas. Intuitively, a heap is represented by a graph where the nodes model objects and the edges model pointers between objects. The heap edges are labeled with symbols from a given alphabet , which stands for the set of all program pointers, including all program variables and record elds (selectors). It is furthermore required that the graph be deterministic, as a program pointer can only point to one object at a time.

In this paper we adopt the storeless representation 2], 12], 14], 8] of a graph, in which each node is associated the language recognized by the automaton whose set of states is given by the set of graph nodes, the transition relation by the set of edges, the initial state is a designated entry point in the heap, and the unique nal state, the node itself. The interested reader is referred to 2] for a detailed discussion on the advantages of the storeless representation of heaps, such as compatibility with garbage collection and isomorphic transformations.

De nition 1 (Heap). A heap M P( + ) is either the empty set or a nite set fX 1 ; X 2 ; : : : ; X n g satisfying the following conditions, for all 1 i; j n: (C1) non-emptiness: X i 6 = ;, (C2) determinism: i 6 = j ) X i \ X j = ;, (C3) pre x closure and right regularity: 8x 2 X i 8y; z 2 + x = yz ) 9 1 k n y 2 X k ^Xk z X i ]]] One can also think of a heap element as the set of all incoming paths leading to it, paths that start with a program variable. The (C1),(C2) and (C3) restrictions must be imposed on the elements of a heap in order to maintain the correspondence (up to isomorphism) with the graph model 2]. An equivalent approach, taken in 14], 8], is to consider the languages in the heap as equivalence classes of a right-regular relation on . The set of all heaps over an alphabet is denoted in the following by H( ).

Figure 1 introduces the abstract syntax (upper part) and semantics (lower part) of the wAL logic. The terms of a wAL formula are regular expressions over the alphabet with free variables from a set V ar. We allow the classical composition operations on regular expressions, together with the left derivate, denoted by ?1 1 2 = f 2 j 1 \ 2 6 = ;g 1 . Formulas are built from the atomic propositions 1 = 2 (language equivalence) and hXi 1 (modality) connected with the classical rst-order operators ^, : and 9. A less usual requirement is imposed on the syntax of the existential quanti er: the quanti ed variable need to occur at least once within the angled brackets of a modality in the scope of the quanti er, which is formally captured by the 'hXi. Notice also that only free variables can occur inside the modality brackets. A formula ' is said to be closed if no variables occur free i.e., FV (') = ;, where FV is de ned recursively on the syntax, as usual. We de ne 8X : ' = :9X : :', ' 1 _' 2 = :(:' 1 ^:' 2 ), and ' 1 ! ' 2 = :' 1 _ ' 2 . The set of all wAL formulas over the alphabet is formally denoted by wAL ].

::= v 2 j X 2 V ar j j 1 2 j j 1 2 j 1 \ 2 j j ?1 1 2 ' ::= 1 = 2 j hX i 1 j ' 1 ^'2 j :' j 9X : 'hXi

] ] = (FV ( ))=FV ( )] 1 = 2 ] ] M; = 1 ( ) 1 ] ] = 2 ] ] hX i 1 ] ] M; = 1 ( ) (X) 2 M and (X) \ 1 ] ] 6 = ; 9X ']] ] M; = 1 ( ) 9 2 P ( ) : '] ] M; X! ] = 1

Fig. 1. Weak Alias Logic

A wAL formula is interpreted with respect to a heap M and a valuation assigning free variables to languages. The only non-standard operator is the modality hXi 1 , where X is bound to denote a heap entity which intersects (the interpretation of) 1 . As a consequence of the syntactic restriction imposed on the existential quanti er, all variables in a closed formula are bound to heap entities 2 . A heap M is said to be a model for a closed wAL formula ' if and only if '] ] M; X:? = 1. In case where ' has at least one model, it is said to be satis able.

At this point, the reader can notice an embedding of wAL into the Monadic Second Order Logic on graphs. Indeed, a wAL formula is composed of equivalences of regular expressions ( 1 = 2 ) related using rst order connectives. Such equivalences can be described by nite automata which, in turn, can be speci ed in MSOL. However, we found using regular expressions, instead of MSOL, more intuitive for the speci cation of heap properties, as it is shown in the following.

Path properties reach(X; Y

) hY iX + next(X; Y ) hY iX ^8Y 0 : hY 0 iX ! Y = Y 0 linear(X; Y ) reach(X; Y ) ^8Z : :Z = Y ^?X = Z _ reach(X; Z) reach(Z; Y ) ! 9Z 0 : :Z 0 = Z ^next(Z; Z 0 ) cycle(X; Y ) reach(X; Y ) ^reach(Y ; X) share(X; Y ) 9Z : reach(X; Z) ^reach(Y ; Z) Recursive data structures nclist(head) 8X : hX ihead ! 9Y : hY iX next ^linear(X; Y ) ^:cycle(Y ; Y ) dlist(head; next; prev) 8X; Y 9Z : (hXihead ) :hY iX prev)( hZ iX next ) X 6 = Z ^hX iZ prev) tree(root) 8X:hX iroot ! 8Y ; Z : (reach(X; Y ) ^reach(X; Z)) ! :share(Y ; Z)) dag(root) 9X : hX iroot ! 8Y ; Z : reach(X; Y ) ^reach(X; Z) ! :cycle(Y ; Z) Fig. 2

. Expressing properties of heaps

The properties in Figure 2 describe various paths in the structure. We consider the predicate reach(X; Y ) stating that node Y is reachable from node X by some non-empty path. A node Y is said to be next to a node X if Y is the only neighbor of X. A path from X to Y is linear if there is no branching i.e., if all the nodes on the path have only one successor. The existence of a cycle containing both X and Y is given by the cycle(X; Y ) predicate.

The wAL logic can also describe the shapes of most typical recursive data structures used in programming languages with dynamic memory allocation: lists, trees, dags, etc. For instance, non-cyclic simply-linked lists pointed to by the head variable and using the next eld as forward selector, are being described by the nclist predicate. Doubly-linked lists pointed to by the head variable and using the next and prev eld pointers as forward and backward selectors, respectively, can be captured by the dlist predicate. Some data structures, such as trees, require the absence of sharing. A sharing predicate expressing that X and Y belong to two structures that share some node can be given by share(X; Y ). A tree structure pointed to by a variable root is described by the tree formula. A dag structure in which every node is reachable from a root variable is given by the dag formula.

Undecidability of wAL

The result of this section comes with no surprise, in the light of similar undecidability results for logics able to express graph properties such as e.g, the logic of Bunched Implications (BI) 5], and Monadic Second-Order Logic of graphs 7]. Given along the same lines as the undecidability proof for BI 5], our proof for wAL relies on a classical result in nite model theory 9], namely that the rst order logic interpreted over nite structures is undecidable.

Given a vocabulary V of relation symbols, let FO V] be the set of rst-order formulas with symbols from V. For each relation symbol R 2 V, let #(R) denote its arity i.e., its number of arguments. Let V = fR 1 ; : : : ; R n g for the rest of this section. We interpret rst-order formulas over structures A = hA; R A 1 ; : : : ; R A n i, where A is the universe and R A i A #(R i ) , 1 i n are the interpretations of the relation symbols from V over A. A structure is said to be nite if and only if its universe is nite. Given a valuation v : FV (') ! A of the free variables in a formula ' 2 FO V], we denote by '] ] A;v the interpretation of ' in A. We say that A is a model of a closed rst-order formula ' if and only if '] ] A; X:? = 1. It is known that the problem of nding a nite model for a closed FO V] formula is undecidable 9]: Theorem 1 (Trahtenbrot's Theorem). Let V be a vocabulary with at least one symbol of arity two or more. Then the set Sat V] = f' 2 FO V] j FV (') = ;; ' has a nite model g is not decidable.

Given an arbitrary rst order formula, we shall translate it into a wAL formula such that satis ability is strongly preserved by the translation. Considering that V = fR 1 ; : : : ; R n g, we de ne V = f i1 ; : : : ; i#(R i ) ; i j 1 i ng f g.

That is, for each relation symbol of arity k we consider k di erent -symbols and a -symbol in V . The translation is given by the recursive function :

FO V] ! wAL V ], de ned as:

(R k (X 1 ; : : :

; X #(R k ) )) = 9X : hX i ^V#(R k ) i=1 hX i iX ki (X = Y ) = X = Y (' 1 ^'2 ) = (' 1 ) ^ (' 2 ) (:') = : (') (9X : ') = 9X : hX i ^ (')
Note that the translation of a closed rst-order formula respects the syntactic constraints of wAL, that each quanti ed variable must occur inside the brackets of a modality, and that only a variable can occur on this position. Moreover, a closed rst-order formula translates into a closed wAL formula. Now it remains to be shown that the translation strongly preserves satis ability. We remind that satis ability for wAL is implicitly de ned on nite models (De nition 1). Due to space constraints, all proofs are deferred to 3]. Lemma 1. A closed rst-order formula ' is nitely satis able if and only if (') is satis able.

Considering for the moment that the alphabet is su ciently large to code the vocabulary V of a given rst order logic, Theorem 1 and Lemma 1 lead immediately to the following result.

Theorem 2. For a su ciently large alphabet , the set Sat ] = f' 2 wAL ] j FV (') = ;; ' has a model g is not recursive.

Since Theorem 1 holds for vocabularies containing at least one relation symbol of arity two, by the de nition of V it follows that Theorem 2 holds for generic heaps over alphabets of size at least four. Here, a more re ned heap model could provide us with more intuition in identifying classes of heaps over which the satis ability problem becomes decidable. For instance, considering = , \ = ;, j j j j = 1 and all heaps of the form M P(

) i.e., heaps consisting only of (possibly circular) singly linked lists. In this simple case, we propose to revisit the decidability of the satis ability problem for wAL.

In order to show that the satis ability problem for wAL is recursively enu- that enumerates all models M 1 ; M 2 ; : : : , testing whether each M i is a model of , will eventually stop.

Lemma 2. For every nite , the set Sat ] is recursively enumerable.

An interesting open problem is then how to nd useful semi-decision procedures for wAL.

Propositional Alias Logic

The negative result from the previous section motivates the search for decidable subsets of wAL that are able to express meaningful properties of heaps. One basic property encountered in many applications is data sharing. In this section we de ne a simpler logic based directly on the notion of aliasing of nite heap access paths (Propositional Alias Logic, or pAL for short). The rest of this paper is concerned with the study of pAL from three perspectives: proof theory, automated reasoning and program logic. The ability of pAL to express other heap properties besides aliasing, is also investigated. Figure 3 de nes the abstract syntax (upper part) and the semantics (lower part) of pAL. The terms are nite words over an alphabet , with w ?1 1 w 2 being the su x of w 2 that, concatenated with w 1 , yields w 2 , if such su x exists, or the empty word , otherwise. The atomic propositions are the pre x test (w 1 w 2 ) and the alias proposition (w 1 3w 2 ). Formulas are built from atomic propositions connected with the propositional operators ^and :. In the syntax de nition, ?

w := v 2 j w 1 w 2 j w ? 1 1 w 2 ' := w 1 w 2 j w 1 3w 2 j ' 1 ^'2 j :' j ? w 1 3w 2 ] ] M = 1 ( ) 9X 2 M : w 1 ; w 2 2 X Fig. 3. Propositional Alias Logic denotes the false literal 3 . The set of all pAL formulas over the alphabet is formally denoted by pAL ].

The semantics of pAL is de ned with respect to a heap M. An alias proposition w 1 3w 2 is true if and only if there exists an element of M such that both terms w 1 ; w 2 belong to it. Note that, since M P( + ), if either one of the terms is , the alias proposition is false. The intended meaning of w3w for some w 2 + , is to say that w is a well-de ned path in the heap. The following semantic equivalence is a trivial check: w 1 3w 2 () 9X : hXiw 1 ^hXiw 2 . The pre x relation w 1 w 2 can be encoded in wAL as w ? 1 1 w 2 6 = ; , where = ; is a possible de nition of the empty word in wAL. These considerations justify the fact that pAL is a subset of wAL. The embedding is proper (pAL ] wAL ]), since e.g. reachability and linearity are not expressible in pAL.

Natural Deduction System

This section introduces a natural deduction system 25] for pAL that proves to be a useful tool in reasoning about aliases. Although later in this paper we adopt the automated reasoning view, as opposed to the proof theoretic, a number of results from this sections are used in the rest of the paper. The system (Figure 4) is that of propositional calculus a la Gentzen (rules ^E, ^I, :E, :I, ?E, ?I) to which we add three rules concerning only alias propositions (sufE, sufI and sym). For these rules we take ? pAL ], x; y; z 2 + and t 2 . xt3y x3x (sufE) x3y yt3z xt3z (sufI) x3y y3x (sym) ' ^ ' (^E) ' ' ^ (^I) ? ' (?E) ' :' ? (?I)

?; :' `? ? `' (:E) ?; ' `? ? `:' (:I) Fig. 4. Natural Deduction System for pAL 3 False could have been de ned as ' ^:' for an arbitrary formula '. However an explicit de nition is preferred for the purposes of the proof theoretic system of Section 3.1.

The natural deduction system presented in Figure 4 exhibits a number of interesting properties: it is sound, complete and, all proofs of alias propositions can be given in a normal form. To formalize these notions, we need further notation. If p is an alias proposition, we say that ? `PA p if and only if there exists a derivation of p with premises in ? that uses only the (sufI), (sufE) and (sym) rules. Otherwise, if is any formula, we say that ? ` if and only if there exists a derivation of with premises in ?. By Th(?) we denote the theory of ?

i.e., the set of all formulas that can be deduced from it i.e., Th(?) = f' j ? `'g.

Given a nite set of alias propositions, there exists a heap that is a model for the entire set. Lemma 3. Let ? be a set of formulas containing a nite number of alias propositions, ? + + be a relation on nite sequences, de ned as x ? y if and only if ? `PA x3y, and H ? be the set fx j x ? xg. Then ? is a total equivalence relation on H ? , and the quotient H ? = ? is a heap. Moreover, j jH ? = ? j j k j j?j j, where k 2 N is a constant.

Note that, for arbitrary sets of formulas, the existence of a model occurs as a consequence of the downward closure property4 .

Expressiveness of pAL

In this section we investigate the expressiveness of the pAL language. We show that any nite heap structure over a nite alphabet can be uniquely characterized by a pAL formula. As a consequence, any nite class of heap structures can be de ned in pAL 5 . This extends our previous result in 2], that pAL has the power to distinguish between any two non-isomorphic heap con gurations6 . However, the far more interesting question, of whether and how could pAL be extended to describe recursive data structures and still preserve decidability, is subject to ongoing and future work.

For the rest of this section, let M = fX 1 ; : : : ; X n g be a given heap. We shall de ne a formula M such that M ] ] M = 1 and, for any other heap M 0 such that M ] ] M 0 = 1, we have M = M 0 . For a nite word w 2 + , we denote by Pref(w) the set of all its pre xes, including w. For a set X 2 M, a word w 2 X is elementary if and only if it has at most two pre xes in X and at most one pre x in any other set Y 2 M, Y 6 = X. Formally, we have Elem M (X) = fw 2 X j j jPref(w) \ Xj j 2 and 8Y 6 = X : j jPref(w) \ Y j j 1g.

An important property of the sets of elementary words is niteness. This results as a consequence of the fact that both M and are nite, since the length of any w 2 Elem M (X) is jwj j jMj j + 1, thus j jElem M (X)j j j j j j j jMj j+1 . A dangling word is a minimal unde ned path in M. Formally, we de ne Dang M (X) = fwa j w 2 Elem M (X); a 2 ; wa 6 2 S Mg. Since Elem M and are nite, so is Dang M (X). With this notation, we de ne: ? M = X2M fw3w 0 j w; w 0 2 Elem M (X)g [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF] X;Y 2M;X6 =Y f:(w3w 0 ) j w 2 Elem M (X); w 0 2 Elem M (Y )g

(2) X2M f:(w3w) j w 2 Dang M (X)g f:(a3a) j a 2 n Mg [START_REF] Bozga | On Logics of Aliasing[END_REF] This set is constructed as follows: the rst component [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF] describes each object as a set of alias propositions composed of elementary sequences, the second component [START_REF] Bozga | Storeless Semantics and Alias Logic[END_REF] distinguishes between objects using negated alias propositions and the third and fourth components (3) describe the dangling sequences. Notice that ? M is not minimal, since for instance in (2) it is su cient to choose only one w 2 Elem M (X) and one w 0 2 Elem M (Y ). However, it is nite, according to our previous considerations. Intuitively, ? M contains all the necessary information to characterize M, thus we shall take M = V ? M . To show that M is a model of M is a trivial but tedious check. That it is indeed the only model, will be shown in the rest of this section. Lemma 4. Let M be a heap with X 2 M, and ? M be the characteristic set de ned in the previous. Then the following hold:

1. for each w 2 X there exists w 0 2 Elem M (X) such that ? M `w3w 0 . 2. for all w 6 2 S M we have ? M `:(w3w). 3. for any x; y 2 + we have x3y] ] M = 1 ) ? M `x3y and x3y] ] M = 0 ) ? M `:(x3y).

Notice that, from the third point of Lemma 4, and since ? M is satis able, hence consistent, we obtain that '] ] M = 1 if and only if ? M `'. Thus, the set of formulas that are satis ed by M is nitely axiomatisable since Th(? M ) = f' j '] ] M = 1g, and ? M is nite by de nition. Theorem 3. Let M be a heap and M be the formula V ? M . If M ] ] M 0 = 1, then M = M 0 . Example Given = fa; b; cg, the heap M = fab g composed of one element pointed to by a with a b self loop is characterized by the formula a3ab ^:c3c: ac3ac.

Tableau Decision Procedure for pAL

A proof that uses natural deduction is mainly based on manually adding assumptions in order to reach contradictions (and deleting them afterwards). This makes, in general, natural deduction unsuitable for automated reasoning and motivates our preference for the method of analytic tableaux 24], an elegant and e cient proof procedure for propositional logic, which we subsequently extend to pAL. Traditionally, a tableau for a propositional formula ' is a tree having '

as the root node and subformulas of ' or negations of subformulas of ' as nodes.

A

Fig. 5. Tableau Expansion Rules

Figure 5 shows the tableau expansion rules for pAL. We consider that x; y; z 2 + and t 2 that is, we can apply the rules also for an empty su x (t = ). The tableau is constructed top-down. A rule whose hypothesis are of the form ' : : : (namely T 1 and T 8 ) can be applied at a node, as soon as both ' and are on the path from the root to the current node, order independent. Rule (T 5 ) expands by putting both ' 1 and ' 2 on the same branch of the tableau, while rule (T 6 ) creates two new branches, one containing ' 1 and the other one containing ' 2 . All other rules expand by appending their conclusion to the current branch. We use rule (T 8 ) to close a branch, since ? does not expand any further. Each rule can only be applied provided that its conclusion does not already appear on the current branch, otherwise the procedure runs the risk of looping forever (for instance, applying one of rules T 3;4 ), without introducing any new formulas7 .

Example Figure 6 presents a sample run of the tableau procedure whose goal is to prove that, for some given k 2 N , k = a3ab ! a3ab k is a tautology. First, we eliminate the implication: k = :(a3ab ^:(a3ab k )) and start the tableau procedure with : k as the root node. To the right of each node occurs the number of the node(s) used in the hypothesis, followed by the name of the rule applied in order to obtain that node. In this example, the tableau closes after k + 6 steps. Branching lacks in this tableau because the rule (T 6 ) is never applied. 2

Fig. 6. Tableau Example

The tableau expansion rules can be easily understood with the natural deduction rules in mind. For instance, rule (T 1 ) can be derived using (sufI), (?I) and (:I). Rules (T 2 ) and (T 3 ) are (sufE) and (sufI), respectively, while (T 4 ) is easily derived using (sym) and (:I). The rest of the rules correspond to the purely propositional part of the natural deduction system and are an easy check. This (and the fact that the natural system is sound and complete) ensures that the tableau rules are sound i.e., if a tableau started with :' closes, then ' is a tautology. The dual implication, if ' is a tautology then every tableau started with :' will eventually close, will be dealt with in the following.

Note that the rules in Figure 5 do not cover the entire pAL syntax from Figure 3: the atomic propositions of the form x y are not considered. The reason is that such propositions trivially evaluate to either true or false and could be eliminated from a formula a priori. For completeness, rules for the pre x test are given in 3]. The rest of this section is concerned with proving that the tableau method is both complete and e ective. To handle the tableau rules in an uniform way, we use the uni ed notation of 24]: let an -rule be one of the rules (T 1:::5 ) and -rule be the rule (T 6 ). We denote the premises of a R-rule by R 1 : : : R n and its conclusions by e R 1 ; : : : e R m , where R = ; . De nition 2. A set of formulas ? is said to be downward closed if and only if it respects the following conditions:

{ for no x; y 2 + , we have x3y; :(x3y) 2 ?, { for any -rule, if 1 ; : : : ; n 2 ?, then e 1 ; : : : ; e m 2 ?, { for any -rule, if 1 ; : : : ; n 2 ?, then either e 1 2 S or : : : or e m 2 ?.

A tableau branch is said to be complete if no more rules can be applied to expand it. A tableau is said to be complete if and only if each of its branches is complete. It is manifest that an open complete tableau branch is a downward closed set. The following technical lemma is key to showing satis ability of downward closed sets. We recall here the de nition of the ? relation from Lemma 3. The following theorem is the main result of this section. Lemma 5. For any downward closed set of formulas ?, :(x3y) 2 ? implies x 6 ? y. Theorem 4. Any downward closed set of formulas containing a nite number of alias propositions is satis able.

The proof of the above theorem uses the model construction technique from Lemma 3. The same method can be moreover used to derive a counterexample of a non-valid formula, starting from an open tableau branch. Before stating our completeness result for the tableau method, let us show that the method is e ective. That is, each tableau procedure started with a nite formula as the root node, using the rules from Figure 5, eventually terminates. Lemma 6. The tableau of a nite formula is nite.

Besides showing termination of the tableau procedure, the above lemma, together with Theorem 4 ensure that the tableau approach is complete.

Corollary 1. If a formula ' is a tautology then every complete tableau starting with :' eventually closes. In the light of the decidability result concerning pAL, we are next investigating the time complexity of the above satis ability problem, and nd that it is NPcomplete. The proof uses Lemma 3 to show that satis ability is in NP, and a reduction from the satis ability problem for a set of boolean clauses with three literals (3-SAT) to show NP-hardness.

Theorem 5. The satis ability problem for pAL is NP-complete.

An E ective Program Logic

In this section we demonstrate the possibility of using pAL as a weakest precondition calculus for imperative programs with destructive updating. Otherwise stated, we show that pAL is closed under applications of the weakest preconditions predicate transformers. Intuitivelly, this is a consequence of the fact that pAL formulas refer to nite portions of the heap, and also that straight-line statements a ect bounded regions of the heap. Our proof of closure is constructive i.e., we de ne weakest preconditions in terms as predicate transformers directly on pAL. This is achieved by means of the sound and complete program logic de ned on top of wAL 2]. Moreover, soundness and completness of the pAL weakest precondition axioms are consequences of soundness and completness in the case of wAL.

We consider a simple imperative language consisting of the following three atomics statements. Note that the statements of most object-oriented languages can be precompiled in this form, possibly by introducing fresh temporary variables:

Stmnt := uv = null j uv = new j uv = w (where uv 6 w) Here v; w 2 denote pointer variables, and u 2 is a (possibly empty) dereferencing path. The rst statement resets the v eld of the object pointed to by u, if u 6 = , or the v top-level variable, otherwise. This may cause the builtin garbage collector recall all non-reachable objects. The second statement allocates a fresh object for further uses, and the third statement assigns its lefthand side the object pointed to by the right-hand side variable. The syntactic constraint that comes with the last statement is due to the following technical problem. The semantics of the assignment is given as the composition of two primitive operations: rst one removes the v arc from the node pointed to by u, and then it assigns it to w. If uv w and there are no other paths to the cell pointed to by w, the garbage collection caused by the rst operation removes the unreachable cell before the assignment is nished. The requirement uv 6 w is however su cient to ensure that, in practice, this situation never occurs.

The axiomatic semantics of this language has been introduced in 2], by de ning a weakest precondition operator g pre on wAL formulas, and is brie y recalled here. For any transition relation over a sequence of statements ! 2 Stmnt + , g pre distributes over conjunction and universal quanti cation i.e., g pre(!; ' 1 ^'2 ) = g pre(!; ' 1 ) ^g pre(!; ' 2 ) and g pre(!; 8X : ') = 8X : g pre(!; '). For total transition relations we have g pre(!; ') ) :g pre(!; :'). If, moreover, the transition relation is total and deterministic, we have that g pre is its own dual i.e., g pre(!; ') , :g pre(!; :'). In the latter case, g pre distributes over disjunction and existential quanti cation too. These properties of g pre for total, deterministic programs allow us to de ne general inference rules for the precondition inductively on the structure of the postcondition. In particular, it is su cient to de ne preconditions only for modalities, the rest of the atomic propositions in wAL being pure i.e., having model-independent denotations. Figure 7 (upper part) gives the precondition of primitive storeless operations add, rem and new for arbitrary modalities. This is generalized to the statements de ned in the previous (lower part).

f9X:X n Sv = T ^hX i( n Sv )g rem(S,v) fhT i g f9X: v (S; T; X) = U ^Wi=1;2 ; i (X; X)g add(S,v,T) fhU i g where v (S; T; X) = X Sv((T ?1 S)v) (T ?1 X)

x;y 1 (X; Y ) = Sv((T ?1 S)v) (T ?1 X) \ x = ; ^hY iy x;y 2 (X; Y ) = Sv((T ?1 S)v) (T ?1 X) \ x 6 = ; ^hY i f(T = Sv ^ \ Sv 6 = ;) _ hT i g new(S,v) fhT i g f9S:hSiu ^g pre(rem(S; v); ')g uv = null f'g f9S:hSiu ^g pre(rem(S; v); g pre(new(S; v); '))g uv = new f'g f9S9T :hSiu ^hT iw ^g pre(rem(S; v); g pre(add(S; v; T); '))g uv = w f'g Fig. 7.

wAL Weakest Preconditions

For the rest of this section, let ; ; ; u; v; w denote constant words, and x; y; z denote variables ranging over words. We introduce the following notation: 9x

: '(x) = W 2Pref( ) '( ). Since is a nite word, so is the formula on the right. Figure 8 We assert that all translations de ned in Figure 8 preserve logical equivalence. To convince ourselves of this fact, let us perform the step-by-step derivation for the positive form of . The rest of the formulas are translated along the same lines.

9S : hSiu ^ 9S : hSiu ^ 2 Sv () 9S : 9x : hSiu ^hSix ^xv () 9x : x3u ^xv

The goal of this section is to prove that the logic pAL is expressive enough to characterize the destructive updating program statements considered in the previous. The following theorem captures the result. Theorem 6. For any sequence of statements ! 2 Stmnt and any formula ' 2 pAL ], we have g pre(!; ') 2 pAL ].

The proof proceeds by deriving the weakest precondition for an arbitrary alias proposition 3 (equivalently written in wAL using the embedding rule) i.e., applying the rules in Figure 7. The result is then translated back from wAL to pAL using the shorthands from Figure 8. Then we can extend the result to arbitrary post-conditions using the distributivity properties for g pre, and to arbitrary sequences of statements by induction on the length of the sequence.

It is important to notice that the translations from pAL to wAL and back are logical equivalences. Since the g pre operators de ned on wAL formulas are sound and complete, according to the development in 2], we can infer the existence of a sound and complete weakest precondition calculus also for pAL.

Conclusions and Future Work

This paper concerns a deductive veri cation method for aliasing properties in imperative programming languages with destructive updating. Starting from previous work on storeless semantics and alias logic with a weakest precondition calculus wAL, we show that the satis ability problem is undecidable but recursively enumerable. Next, we focus on a decidable subset pAL that allows to express sound and complete weakest preconditions. The kind of properties expressible in this logic are related to pointer aliasing, but also arbitrary nite heaps can be de ned. We give two sound and complete proof systems for pAL, one based on natural deduction, and another based on analytic tableaux. The satis ability problem for pAL is shown to be NP-complete. A tool based on the pAL framework is planned in the near future.

The main question related to the existence of a decidable program logic that can express non-trivial shape properties of heap is not fully answered. Although undecidable, the wAL logic o ers a reach framework in which one can de ne decidable fragments having complete weakest precondition calculi. One such example is pAL. A still open question is the existence of a fragment of wAL that encompasses pAL, in which one can express properties such as reachability, circularity, etc. One such extension, called kAL, is currently under investigation. This logic is obtained from pAL, by considering words (over the heap alphabet) with integer counters (parameters indicating the repetition of a nite subword) and rst order quanti cation over the counters. In this way we can express for instance the existence of an unbounded next-path between two pointers head and tail: 9k : head:fnextg k 3tail, a property that is not expressible in pAL. We plan an extensive study of this logic, in order to cover both aspects of satis ability and expressiveness.

M 2 H

 2 ( ); : V ar ! P ( )

  tableau branch is said to be closed if it contains a formula together with its negation, and open otherwise. A tableau is said to be closed if and only if all its branches are closed. To check whether a formula ' is a tautology one builds the tableau for :', and infers that ' is a tautology if and only if the tableau eventually closes. In case at least one branch remains open, a counterexample for ' can be extracted.

	:(xt3z) : : : yt3z :(x3y)	(T 1 )	xt3y x3x (T 2 )	x3y y3x (T 3 )	:(x3y) :(y3x)	(T 4 )
	' 1 ^'2 ' 1 ; ' 2 (T 5 )		:(' 1 ^'2 ) :' 1 j :' 2	(T 6 ) ::' ' (T 7 )	' : : : :' ?	(T 8 )

  introduces a number of syntactic shorthands, providing context-dependent translations from wAL to pAL for them. That is, we do not translate the shorthands individually, but rather in an existentially closed context.

	De nition : 2 Sv	wAL 9S : hSiu ^ 9S : hSiu ^: 9S9T 9X : hSiu ^hT iwĥ 9x u3u ^:(9x Xi ^ 9x	pAL : x3u ^xv : x3u ^xv ) : x3u ^xv ŵ((xv) ?1 )3
	: 2 Sv(T ?1 X)	9S9T 9X : hSiu ^hT iwĥ Xi ^: u3u ^w3w ^ 3 :(9x : x3u ^xv ŵ((xv) ?1 )3 ) 9S9T : hSiu ^hT iw ^ 9x 9y (xv) ?1 : x3ux v ^wy3u ^yv (xv) ?1
	: 2 Sv(T ?1 S)v	9S9T : hSiu ^hT iw ^:	u3u ^w3w: 9y (xv) ?1 : x3ux v ^wy3u ^yv (xv) ?1 ) (9x
	Fig. 8. wAL to pAL translation shorthands

Intuitivelly, we need the left derivate to describe paths between two objects in the heap. If X and Y are two objects in a heap, then X ?1 Y is the language of all paths between X and Y .

This syntactic restriction on the quanti cation domain was mainly suggested by the fact that, allowing quanti cation over P ( ) makes the logic undecidable even when modalities are not used at all in formulas. A formal proof will be included in an extended version of this paper.

De nition 2 in Section 4.

Even if a pAL formula, e.g x3y, is in general satis ed by an in nite number of heaps.

There we proved ony that two structures are isomorphic if and only if they are models of the same pAL formulas.

The de nition of a ner notion of redundancy is planned in the full version.


Philippe Askenazy

Thomas Breda

Flavien Moreau

Vladimir Pecheu

Do French companies under-report their workforce at 49 employees to get around the law?

The Institut des politiques publiques (IPP) was created by PSE and developed through a scientific partnership between Paris School of Economics (PSE) and Groupe des écoles nationales d'économie et de statistique (GENES). The aim of the IPP is to promote quantitative analysis and evaluation of public policy using cutting-edge research methods in economics. Do French companies under-report their workforce at 49 employees to get around the law?

Various legal obligations in terms of social dialogue, profit sharing and accounting apply to French companies when they reach the threshold of 50 employees. This policy brief shows that a significant proportion of companies voluntarily under-report their workforce below this threshold and this allows them to avoid their obligations.

Compliance with the law in terms of social dialogue or profit-sharing thus appears to be linked to the number of employees that companies declare and not to their actual workforce. These results illustrate how the labor code can be circumvented in a complex regulatory environment and in the absence of sufficient means of oversight.

They invite reflection on the use of more direct and effective methods of monitoring compliance with the law. They also invite caution in considering the results of several recent studies that quantify the cost of legal obligations at the 50-employee threshold, assuming that they are fully respected in practice.

Far more French companies declare 49 employees than 50 employees in their tax returns. This spike at 49 employees is often attributed to the additional obligations that are triggered at the 50-employee threshold: companies may refuse to cross this "social threshold" in order to avoid, for example, having to set up a works council. This reduced growth of companies would ultimately limit productivity and employment.

However, when the workforce is calculated directly from administrative data on all employees, the spike at 49 employees disappears entirely. Thus, it is the workforce reported by the employer and not the actual number of employees that spikes at 49. We suggest that this phenomenon is explained by the fact that the legal workforce is difficult to calculate and is not public, so that compliance with certain legal obligations depends in practice on the declared workforce.

The cost of misreporting appears to be low, so that companies that fear legal obligations have everything to gain by misreporting their workforce and thus avoiding these obligations.

These results partly challenge the evidence associating workforce thresholds with a deleterious effect on growth.

Workforce thresholds: An exorbitant cost?

Depending on the number of employees, French companies must fulfill a certain number of legal obligations: setting up a works council, profit-sharing with employees, certification of accounts by an auditor, etc. These obligations are generally triggered by company size thresholds, often referred to as social thresholds because they entail obligations mainly in terms of social dialogue.

Several studies have looked at the potential cost of these thresholds for companies and their effect on growth. They attempt to estimate the economic cost of legal obligations (Gourio and Roys, 2014; Garicano, Lelarge, and Van Reenen, 2016), their effect on the share of labor in added value (Smagghue, 2020), or their effect on innovation (Aghion, Bergeaud, and Van Reenen, 2021). Garicano, Lelarge, and Van Reenen, 2016 estimate that the obligations applying to the 50-employee threshold alone would have a staggering economic cost: 3.4% of GDP, or €92 billion in 2019.

The starting point for these analyses is the existence of a spike at 49 employees in the distribution of the number of firms, followed by a trough at 50 employees and above (Figure 1a). The spike suggests that many firms do not wish to cross the threshold, which would be costly for them. Regulations at the 50-employee threshold could not only affect the growth of some companies just below the threshold, but also induce significant additional economic costs for all those whose workforce is already above the threshold, and which should therefore in theory have implemented the legal obligations. The abovementioned studies attempt to quantify this overall cost using economic equilibrium models estimated by exploiting distortions in the distribution of company size.

The authors of the studies cited above generally use the number of employees provided by employers in their tax returns as a measure of firm size. Since this workforce is declared by the employer, it can be manipulated. However, it is also possible to reconstitute the size of firms from the payroll records of each employee. This second measure of the workforce is difficult for the employer to manipulate as long as his employees have an employment contract and receive a salary. However, when this second source is used, in which the size of firms is measured rather than declared, the spike at 49 employees disappears and the distribution of firm sizes seems relatively smooth around the 50-employee threshold. 1 The aim of this policy brief is to offer a comprehensive explanation for the discrepancies between sources. To do so, we focus on the different ways in which company size 1 This difference between sources has already been noted by Ceci-Renaud and Chevalier, 2010, who were, however, unable to fully understand the cause. can be measured and how legal requirements are applied and monitored in practice.

Distribution of the declared and recalculated workforce at around 50 employees

Figure 1a shows the proportion of French firms reporting each employee size between 30 and 70 in 2006. The workforce variable considered is the average of the total number of employees at the end of each quarter of the current accounting period (regardless of their status, seniority and workload). It is reported by the employer and we observe it in the FICUS tax data, which is an aggregation by the national statistics bureau (Insee) of data from different tax regimes (see Box 1).

Figure 2b reproduces the same exercise for the same year, but this time considering the average full-time equivalent (FTE) workforce over the year, as reconstructed by Insee from the annual declarations of employee data (DADS) (see Box 1). The number of employees is not declared by the employer but is calculated by adding up the number of employees for whom a company pays social security contributions. The filing of DADS is mandatory. Erroneous declarations expose the company to heavy fines, both variable (as a percentage of the amount omitted) and fixed (per erroneous or omitted line). In addition, since 2006, payroll software must automatically produce the DADS declaration to be transmitted to the administration (DADS-U standard). It can therefore be considered that the DADS provide a portrait of a company's workforce that is difficult to manipulate by the employer. When the Insee measure constructed from this source is used, the jump to 49 employees is no longer visible. 2 Companies are also obliged to file their accounts with the commercial court registries, and by default these must be identical to tax returns filed with the tax authorities. Although the commercial courts have a diverse legislative arsenal at their disposal to enforce the obligation to file annual accounts, sanctions are rare in practice. Companies do, however, have incentives to file their accounts to provide information that many of their lenders, customers or suppliers consider useful before entering into a business relationship. These filed accounts are then made public and collected in a DIANE database (see Box 1) for commercial purposes. Except in the (in practice rare) case in which a firm has filed different accounts with the tax authorities and the commercial court clerks, the DIANE data are identical to the FICUS tax data. Interpretation: A significant jump to 49 employees appears for the workforce declared in the unadjusted tax data (FICUS and DIANE), but it is non-existent for the FTE workforce recalculated by Insee from DADS data.

In Figure 1c, we see that for firms that have agreed to make their accounts and workforce public (about 75% of firms around the 50-employee threshold), there is a spike in the number of firms with 48 and 49 employees, and a drop in the number of firms beyond that.

Our online working paper reproduces the same figures for more recent years. From 2008 onwards, the spike at 49 employees in the data reprocessed by Insee is much less significant. In fact, Insee reprocessed the original declarative variable in the FARE-ESANE system, the successor to FICUS, because it judged its quality to be too limited, and even advised against using it for statistical processing.

Deliberate under-reporting of the workforce...

To what extent does the spike at 49 employees in the distribution of the workforce reported by employers reflect intentional under-reporting?

To answer this question, we used DADS social security data to construct a new, non-manipulable measure of the workforce that corresponds exactly to the definition of workforce in the tax data. This exercise is made possible by the exhaustive nature of the DADS dataset, which makes it possible to observe each year for each job in each company, the start and end dates of the job observed, as well as the corresponding number of hours worked. We were thus able to recalculate the number of employees present in a given company at the end of each quarter of the current fiscal year, then take the arithmetic average of these numbers over the year to obtain a measure of the workforce strictly equivalent to the definition of the workforce reported in the accounting data. Figure 2a shows the distribution of this "fiscal" workforce, as recalculated for 2006, between 30 and 70 employees: this distribution does not show any spike at the 50-employee threshold (with identical results for other years). Note: Workforce variables reconstructed by the authors from DADS data and rounded down in the graphs. Interpretation: Whichever concept of workforce is used (average number of employees present at the end of each quarter or the FTE number over the year), the distribution does not show a jump or discontinuity around 50 employees.

To examine whether firms are strategically underreporting their workforce, we compare the workforce reported in the tax data to the equivalent that we have reconstructed. Figure 3a thus shows for each reconstructed firm size between 30 and 70 employees and for the years 2002 to 2015, the proportion of firms that report a workforce that is (i) the same as, (ii) larger than, or (iii) smaller than the reconstructed workforce. We observe that the proportion of firms declaring their workforce correctly is low: between 10% and 20%, regardless of the size of the firm considered. More firms under-report their workforce (between 50% and 70%) than over-report it (between 20% and 40%).

The central feature of Figure 3a, however, is the way in which the mismatch between the two workforce measures varies at the 50-employee threshold: the proportion of firms under-reporting their workforce rises sharply around the 50-employee threshold, from about 50% to 70%. This suggests that the difference between declared

FICUS tax data (2000-2007).

The FICUS data come from the tax returns of companies subject to the industrial and commercial (BIC) and non-commercial (BNC) tax regimes. In addition to an income statement and balance sheet data, firms report, in an appendix, their workforce for the accounting period. This is calculated as the arithmetic average of the number of employees at the end of each quarter of the fiscal year. This is the total number of people with employment contracts who are paid directly by the company, and therefore excludes temporary workers.

DIANE tax data (2002-2015). DIANE data are collected by the private company Bureau Van Dijck from the commercial court registries. Companies are required to file their tax returns with the commercial court register, under penalty of sanctions. These filed accounts are then public, except for micro-businesses that can since 2014 choose a confidentiality clause, and since August 7, 2016, for small companies with an average declared workforce of less than 50 employees. Except in the case in which a company has filed different accounts with the tax authorities and the commercial courts, the DIANE data is identical to the FICUS tax data.

FARE tax data (2008-2015).

The FARE data contain accounting information from tax returns that are consistent with information from the Annual Sectoral Survey. In addition to businesses subject to the BNC and BIC regimes, FARE contains data on agricultural businesses under the BA regime. FARE contains the same accounting information as FICUS, but unlike FICUS, the FARE workforce data is reprocessed by Insee, with the algorithm described in Insee2012.

DADS social security data (2002-2015).

In the 'postes' section of DADS, employers provide the start and end dates of the pay period for each employee, as well as the number of hours worked. This information is used to recalculate the workforce measures.

MARS workplace election reports (2009-2016).

The MARS data come from the processing of the minutes of the workplace elections for works councils and staff delegates that took place in companies with least 11 employees over both the 2009-2012 and periods. They make it possible to identify firms that have a works council from 2012 onwards.

Box 1: Data used to measure the number of employees and the obligations at the 50-employee threshold Box 1: Data used to measure the number of employees and the obligations at the 50-employee threshold and reconstructed workforce numbers is not simply due to a slight difference in the workforce concepts used, or to approximations by employers who may not know their exact workforce numbers. Indeed, if this were the case, we should not observe a jump in the probability of under-reporting exactly at the threshold where this under-reporting may be of interest, as we will show.

In Figure 3b, we take this exercise a step further and examine by size the proportion of firms that under-report their workforce relative to the reconstructed workforce by 1 to 6 employees. We observe a staircase profile: the proportion of firms under-reporting by 1 employee jumps to 50 employees, the proportion under-reporting by 2 employees jumps to 51 employees, and so on. Whatever its magnitude, the under-reporting of the reported workforce in relation to the reconstructed workforce is most noticeable when it keeps the former at exactly 49 employees. This phenomenon of under-reporting continues to be observed in a statistically significant way up to firms with more than 70 employees. 3 The proportion of firms under-reporting their workforce increases sharply around the 50-employee threshold.

... which can help avoid legal constraints

Why would companies have an interest in underreporting their workforce to the tax authorities when they exceed 49 employees? The answer we suggest is that they can avoid the social regulations that apply above the threshold, without facing any particular risk.

The cost of such behavior is first of all low because the number of employees mentioned in the tax returns has no direct impact on corporate taxation. Unlike the DADS, an erroneous declaration cannot generate a tax penalty and is therefore not information on which tax inspectors focus their attention. Nor is it of interest to labor inspectors or social security collectors (Urssaf), since all the provisions of the labor or social security codes are based on other concepts of company size (see the working paper associated with the policy brief). As for the official statisticians, they are content to note the poor quality of the declarative variable.

Under-reporting your workforce on tax forms is therefore not very risky. But what do companies have to gain?

The important point here is that even if the declared workforce does not correspond exactly to the legal workforce on which the implementation of regulations is based, it is most often the only publicly available information on the size of the company. Although commercial databases containing accounts filed with the commercial court registries are subject to a fee, they generally provide the class of the company free of charge, and thus whether their declared workforce is above 50 employees. The information is available on sites such as societe.com. A trade union seeking to establish itself in companies without a works council will only have access to these public sources to determine the target companies. Within companies, in a context in which the legal workforce is difficult to calculate and the administration does not directly use other sources to enforce legal obligations, the declared workforce accessible online may become the one used by employees to request the application of regulations that come into force beyond 50 employees.

ture a phenomenon of deliberate under-reporting at the 50-employee threshold.

Regulations enforced on the basis of declared rather than actual workforce

To support this thesis, we attempt to examine the level of compliance with the regulations theoretically applying to the 50-employee threshold as a function of two workforce variables: the workforce declared by employers and a measure of the reconstructed workforce of companies that comes as close as possible to the legal workforce that should serve as the basis for compliance with the labor code.

The regulations that apply to the 50-employee threshold are described in detail in the working paper that accompanies this policy brief: among the most important are the establishment of a works council and an employee profitsharing plan.

These two obligations, like all those included in the labor code and the social security code, are based on a different concept of workforce to that declared in the tax data. This is the FTE workforce during a given period. Specifically, since 2001 and until the PACTE law of 2019, companies must calculate their workforce in FTE month by month.

They have one year to comply with their new obligations in terms of social or labor law when their FTE workforce has exceeded 50 employees for at least 12 months during the previous three years. The law suggests that verification should be done every month, and that the first month that the above condition is verified starts the clock for the implementation of the obligations.

The great richness of the DADS data allows us once again to construct a workforce variable as close as possible to the legal workforce variable described above. First, we ignore the dynamic complexity of the regulations and construct an FTE workforce for each calendar year. We sum the total number of employees observed in each firm in a given year, weighting them by the ratio between the number of hours they worked over the year and the number of hours corresponding to a full-time job over the year in the sector considered. 4 Our measure (for which the distribution is presented in Figure 2b) corresponds to the same concept of workforce as that used for the labor and social security code regulations, with one exception: the legal workforce includes temporary workers present in the company in FTE, whereas our measure excludes them, as these workers are attached to their temporary employment agency and not to their place of work in the DADS.

Our measure of the legal workforce in FTE is therefore an underestimation when temporary workers are present in the firm. For this reason, it should be considered as a lower bound of the actual legal workforce, so that all companies with 50 or more employees according to our FTE workforce measure should normally implement the obligations.

To measure the presence of a works council, we use the MARS data containing, for the 2009-2016 period, the reports that companies must send to the administration when they organize workplace elections. 5 By combining the information contained in MARS on the dates of the elections and the duration of mandates, we were able to construct a variable indicating the presence of a works council for the years 2012 to 2016. 6 It is clear from the left-hand graph of Figure 4 that the proportion of companies having active works council (or attempting to organize an election) the following year jumps sharply, from around 25% to 60%, when the declared size exceeds 49 employees: thus it is indeed the company size that employers declare in the tax data that triggers the setting up of works councils. If we consider the size reconstructed in FTE, which corresponds to the concept of workforce that should trigger the legal obligations, there is practically no jump at 50 employees (Figure 4, right-hand graph). 7 Note: The sources used are described in Box 1. Interpretation: The probability of the presence of a works council rises sharply when the workforce declared for tax purposes by the employer (average number of employees present at the end of each quarter) exceeds the 50-employee threshold. This is not the case when the FTE headcount, on which the establishment of works councils should legally be based, exceeds the threshold.

These results confirm the idea that companies can avoid their legal obligations by under-reporting their workforce. 5 It cannot be totally excluded that some companies have not sent their report to the administration but still have a works council. This phenomenon is not likely to be more prevalent in companies that declare 49 employees.

6 It happens quite frequently that there are no candidates for workplace elections. In this case, the company must report this absence to the administration and we then consider that it has fulfilled its legal obligations for the duration of the mandates corresponding to the election in question. 7 In practice, the obligation to set up a works council at 50 employees or more applies not only at company level but also at each of a company's sites. To facilitate interpretation, we have focused on companies with a single workplace. However, the results are similar when we also include companies with several premises, assuming that they have a works council if one of their premises has one.

They also show a high level of non-compliance with legal obligations: all companies declaring 50 or more employees have not necessarily set up a works council.8 This is particularly the case for companies with exactly 50 employees, which fall between those with 49 and 51 employees. Additional analyses suggest that some of these companies may not have set up a works council because their managers or employees wrongly believe that the obligations are triggered from 51 employees and upwards, not from 50 employees.

For profit-sharing, we make direct use of the amounts paid out as reported in the tax data. Figure 5 shows a similar phenomenon to that observed for works councils: the proportion of companies that make profit-sharing payments jumps when the company declares more than 50 employees, but not when it actually has more than 50 FTE employees.9 This confirms that the implementation of the main legal obligations at the 50-employee threshold depends on the workforce declared by the employer, even though this does not correspond to the concept of workforce used by the law for these obligations. Note: The sources used are described in Box 1. Interpretation: The payment of profit-sharing is highly dependent on the workforce declared by the employer and not the FTE workforce on which it should legally be based.

These results confirm the idea that companies can avoid their legal obligations by under-reporting their workforce.

Small is beautiful?

For several decades, national and local authorities have sought to promote a network of small businesses in France. Crossing the 50-employee threshold therefore not only implies new regulations: it may also mean loss of eligibility for certain local or national aid or exemptions for "small businesses". Thus, companies may not want to grow -or appear to have grown -not because new obligations are being imposed on them, but because opportunities for public support are being removed. For example, new hires are exempt from social security contributions for one year for companies with fewer than 50 employees in rural revitalization zones. Vacation vouchers are also exempt from social security contributions for up to €400 per employee in companies with fewer than 50 employees.

Information on the received and social security contributions paid is available in the tax data, which makes it possible to study changes in relation to the actual and declared workforce. The results (detailed in the working paper on which this policy brief is based) do not reveal any strong discontinuity in the prevalence of aid when firms declare more than 50 employees. On the other hand, we do observe a slight jump in the weight of social security contributions at the threshold of 50 declared employees (but not at the threshold of 50 employees in our FTE recalculation), suggesting that the loss of these exemptions could play a role in staying below the threshold.

Are companies that under-report their workforce different?

Are companies that avoid certain legal obligations by under-reporting their workforce the worst performers and thus the ones that the potential cost of regulations the most? To examine this question, for each available year we construct two groups of firms:

• A group that under-report, comprising companies with a reconstructed workforce of between 50 and 55 employees and a declared workforce of less than 50 employees

• A group that do not under-report, comprising companies with a reconstructed workforce of between 50 and 55 employees and a declared workforce of 50 or more employees

We then examine how the economic performance, financial performance and workforce of the companies in the two groups evolve over time. The results (detailed in the working paper on which this policy brief is based) show that firms that under-report their workforce are smaller (their actual workforce is smaller) and are less likely to have crossed the 50-employee threshold in the past. They also have lower economic performance but higher financial performance than firms that do not under-report. These differences observed at the time of under-reporting are not one-off: they were already present 5-10 years before the time of under-reporting, and they remain in part thereafter, although some of them tend to fade, notably the differences observed in terms of financial performance.

Does under-reporting limit company growth?

Under-reporting at 49 employees for tax purposes is likely to become increasingly difficult as the actual number of employees grows. Even if the penalties are limited, it is obviously harder for a company with 70 employees to claim it has 49. A company might therefore be tempted to limit its growth in order to keep its workforce at a level that would allow it to maintain its declared workforce at 49 in a relatively plausible way. This means that the 50employee threshold could be detrimental to the actual growth of firms, even when they have the opportunity to under-report their workforce by a few units.

This hypothesis does not seem to be supported empirically. Indeed, the size gap between firms that underreport and those that do not under-report does not increase over time from the point at which under-reporting is measured. Firms that try to stay below 50 reported employees thus appear to have real growth comparable to the others.

Discussion

This policy brief shows that companies can under-report their tax-declared workforce without fear of sanctions and without necessarily being audited. A certain number of them indeed do so when they cross the threshold of 50 employees. This under-reporting behavior allows them to temporarily avoid the legal obligations that apply to the threshold, but it does not seem to affect their performance or growth potential.

Why under-report? First, the implementation of the obligations represents an immediate administrative cost for the company manager. In particular, a manager may not want to pay these costs if the workforce exceeds the threshold only to cope with a temporary increase in activity. 10 Second, the implementation of obligations leads to a loss of exclusive control by the managers over the company since they allow employees or the public authorities to be more involved in the management of the company. Some managers may be reluctant to accept these constraints on their decision-making power. Thus, even if legal obligations do not necessarily represent a cost for the company and its stakeholders as a whole, there are many more personal reasons why executives or HR managers may want to postpone implementation.

More generally, it should be remembered that regulations implemented by the public authorities are not a priori intended to only induce additional costs for companies. In general, they have benefits for certain stakeholders: more frequent audits can help avoid undeclared work, credit constraints could limit defaults, works councils could lead to a more equitable distribution of the firm's profits, etc. While these supposed positive externalities are not necessarily proven, they also deserve to be evaluated before normative conclusions can be drawn about the overall effect of regulations. This requires a specific analysis of each of the measures imposed at the 50-employee threshold, rather than a black box approach that attempts to quantify the overall cost of a set of measures that are all assumed a priori to be bad.

The evidence of under-reporting behavior that allows companies to circumvent labor law invites us to rethink the way in which legislators ensure compliance with the law. The implementation of complex regulations, based on concepts of workforce that are difficult to measure, combined with the absence of sufficiently well thoughtout monitoring procedures, largely explain the situation we have observed. The public authorities could, for example, systematically mobilize reliable data sources, as we are attempting to do here, to monitor the size of firms and enforce compliance with labor law.

Figure 1 :

 1 Figure 1: Distribution of the workforce of companies in 2006 according to different sources

Figure 2 :

 2 Figure 2: Distribution of companies' workforce recalculated by the authors in 2006

Figure 3 :

 3 Figure 3: Difference between declared and recalculated workforce using the same definition according to firm size

Figure 4 :

 4 Figure 4: Presence of works councils in the company the following year according to the workforce declared by the employer and the reconstructed legal workforce

Figure 5 :

 5 Figure 5: Profit-sharing payments in the following year according to the workforce declared by the employer and the reconstructed legal workforce

Figure1bshows the graph for the FTE workforce reconstructed by Insee. Insee also calculates the number of employees present on De-

cember 31. The distribution of this alternative measure likewise does not show a discontinuity at 49 employees.

If we look at over-reporting by a fixed number of employees (e.g. 1 employee), we do not observe the same staircase pattern, suggesting that there is nothing mechanical about the results presented here. In the paper that accompanies this policy brief, we produce additional analyses to validate the fact that even in the case of noisy DADS data, we cap-

See our working paper for details. The definition of the FTE workforce proposed by Insee in the DADS excludes jobs with too few hours worked or with too low a salary, even though all jobs must be considered to calculate the legal workforce. This is why we had to reconstruct a measure of the FTE workforce.

In our working paper, we present several additional analyses with a particular focus on accounting for the dynamic aspects of the law. All of them confirm a limited level of compliance with legal obligations.

The fact that

100% of companies to the right of the threshold do not pay profit-sharing can also be explained by the fact that only companies making a profit are required to make profit-sharing payments. However, the same analysis of firms with a positive result changes the results only marginally.

The PACTE law should partially remove this motivation by making certain obligations, including profit-sharing, conditional on exceeding the threshold for five consecutive years.

Authors

Philippe Askenazy is a senior researcher at CNRS-Centre Maurice Halbwachs-ENS-PSL. Thomas Breda is a research fellow at the CNRS affiliated with Paris School of Economics and director of the Labor Program at the Institut des politiques publiques. Flavien Moreau is an economist at the International Monetary Fund. The views expressed in this policy brief are those of the authors and do not necessarily represent the views of the IMF, its executive board, or IMF management. Vladimir Pecheu is a postdoctoral fellow at Aix-Marseille School of Economics.

Reference studies

The arguments developed here are taken from Askenazy et al ( 2022


Marius Bozga
email: fbozga@imag.fr

Susanne Graf
email: graf@imag.fr

Laurent Mounier
email: mounierg@imag.fr

Automated validation of distributed software using the IF environment

This paper summarizes our experience with IF, an open validation environment for distributed software systems. Indeed, face to the increasing complexity of such systems, none of the existing tools can cover by itself the whole validation process. The IF environment was built upon an expressive intermediate language and allows to connect several validation tools, providing most of the advanced techniques currently available. The results obtained on several large case-studies, including telecommunication protocols and embedded software systems, con rm the practical interest of this approach.

Introduction

Automated validation of distributed software is a desirable objective to improve the industrial production of correct systems like communication protocols or embedded systems. In spite of the numerous on going researches and tool developments carried out in this area, this activity remains di cult in practice: on one hand the initial software description is usually provided in a high-level formalism (either a programming language or a formal design notation like Lotos 23], Sdl 25] or Uml 30]), and, on the other hand, a wide range of tools are necessary to cover the whole development process, operating at di erent levels of program descriptions. Even if several interesting tools are currently available, either commercial or academic ones, none of them can ful ll in itself all the practical needs. Commercial tools (such as ObjectGeode 32], Tau 1], StateMate 22], Rational Rose 31], etc.) provide several development facilities, like editing, code generation and testing. However, they are usually restricted to basic veri cation techniques (exhaustive simulation, deadlock detection, etc) and are \closed" in the sense that there are only limited possibilities to interface them with others. On the other hand, there exist numerous academic tools (like Smv 28], Hytech 19], Kronos 34], Uppaal 27], Spin 20], InVeSt 2], etc.) o ering a broad spectrum of quite e cient veri cation facilities (symbolic veri cation, on-the-y veri cation, abstraction techniques, etc.), but often supporting only low-level input languages. This may restrict their use at an industrial scale. This situation motivated the development of IF, an intermediate representation for distributed software together with an open validation environment. This environment ful lls several requirements. First of all, it is able to support di erent validation techniques, from interactive simulation to automatic property checking, together with test case and executable code generation. Indeed, all these functionalities cannot be embodied in a single tool and only tool integration facilities can provide all of them. For a sake of e ciency, this environment supports several levels of program representations. For instance it is well-known that model-checking veri cation of real life case studies usually needs to combine di erent optimization techniques to overcome the state explosion problem. In particular, some of these techniques rely on a syntactic level representation (like static analysis and computations of abstractions) whereas others techniques operate on the underlying semantic level. Another important feature is to keep this environment open and evolutive. Therefore, tool connections are performed by sharing either input/output formats, or libraries of components. For this purpose several well-de ned application programming interfaces (apis) are provided. The IF validation environment is quite similar in its philosophy to the one proposed in the Bandera project 12], which also relies on a dedicated intermediate format to translate (abstract) Java source code into the input language of existing model-checkers (like Spin or Smv). However, currently we mainly address with IF distributed software validation from design formalisms (like Sdl or Uml) which are widely used in the application area we consider (communication protocols and embedded systems).

Architecture

The IF validation environment relies on three levels of program representation: the speci cation level, the IF intermediate level, and the Lts semantic model level. Figure 1 describes the overall architecture and the connections between the toolbox components.

The speci cation level is the initial program description, expressed for instance using an existing language. To be processed, this description is (automatically) translated into its IF representation. The main input speci cation formalism is Sdl, but connections with other languages such as Uml, Lotos and Promela are envisaged.

The intermediate level corresponds to the IF representation 8]. In IF, a system is expressed by a set of parallel processes communicating either asynchronously through a set of bu ers, or synchronously through a set of gates. Processes are based on timed automata with deadlines 3], extended with discrete variables. Process transitions are guarded commands consisting of synchronous/asynchronous inputs and outputs, variable assignments, and clock settings. Bu ers have various queuing policies ( fo, stack, bag, etc.), can be bounded or unbounded, and reliable or lossy. A well-de ned api allows to consult and modify the abstract tree of the IF representation. Since all the variables, clocks, bu ers and the communication structure are still explicit, high-level transformations based on static analysis (such as live variables computation) or program abstraction can be applied. Moreover, this api is also well suited to implement translators from IF to other speci cation formalisms. The implicit enumerative representation consists in a set of C functions and data structures allowing to compute on demand the successors of a given state (following the Open/C sar 16] philosophy). This piece of C code is generated by the if2c compiler, and it can be linked with a \generic" exploration program performing on-the-y analysis.

In the symbolic representation sets of states and transitions of the Lts are expressed by their characteristic predicates over a set of nite variables. These predicates are implemented using decision diagrams (Bdds). Existing applications based on this api are symbolic model-checking and minimal model generation.

Finally, the explicit enumerative representation simply consists in an Lts le with an associated access library. Although such an explicit representation is not suitable for handling large systems globally, it is still useful in practice to minimize some of its abstractions with respect to bisimulation based relations.

Components description

We brie y present here the main components of the environment, together with some external tools for which a strong connection exists.

The speci cation level components. ObjectGeode 32] is a commercial toolset developed by Telelogic supporting Sdl, Msc and Omt. In particular, this toolset provides an api to access the abstract tree generated from an Sdl speci cation. We have used this api to implement the sdl2if translator, which generates operationally equivalent IF speci cations from Sdl ones. Given the static nature of the current version of IF, this translation does not cover yet the dynamical features of Sdl (e.g., process instances creation).

The intermediate level components. if2if 6] implements several algorithms based on static analysis to transform an IF speci cation. A rst transformation concerns dead variable resetting (a variable is dead at some control point if its value is not used before being rede ned). This optimisation can be also applied to bu er contents (a message parameter is dead if its value is not used when the message is consumed). Although very simple, such optimisation is particularly e cient for state space generation (reductions up to a factor 100 were frequently observed), while preserving the exact behaviour of the original speci cation

Case studies

The IF environment was used in several case studies, including as well telecommunication protocols and embedded software. The most relevant ones, from the complexity point of view, and the results obtained are summarized below.

SSCOP Protocol

The Sscop (Service Speci c Connection Oriented) protocol is standardized under reference itu-t q2110 24]. Originally, it was conceived to reliably transfer data between two high bandwidth network entities. Although its design makes it ready to treat signi cant volumes of data, currently its use is con ned in ones of the underlayers of the aal layer (Atm Adaptation Layer). The services it provides are connection control (establishment, ow-control, release), data transfer, and error detection.

The Sscop standardization document contains an Sdl description of the protocol. This description has been coded by France Telecom R&D using ObjectGeode. It consists in approximately 2000 lines of Sdl textual code which describes the protocol as one single process with 10 control states, 134 variables, and 4 timers. The description was centered on signaling and some simpli cations have been made according to Sscop implementations available in France Telecom R&D. Our main goals were the formal validation of the specication and, in addition, automatic test-case generation starting from it. Clearly, the size and complexity of this speci cation made any brute force validation approach not applicable. In particular the data part was very large, and each state of the underlying model could not be stored in less than 2kB. Therefore only a small part of the state space could be explored from this initial speci cation, not su cient to verify interesting properties. Consequently, we adopted a more incremental veri cation strategy. A rst step was to apply a very rough abstraction by (automatically) eliminating all the variables in the speci cation. Thus, it was possible to compare this very abstract speci cation with the one supplied by the standard to model the interactions between adjacent layers of Sscop, to check if the abstract speci cation provides at least the expected behaviour. This comparison was performed using Aldebaran, with respect to the so-called safety preorder 5]. Some subtle errors, such as omission of timers setting, were found using this method. After this debugging phase, the second step was to \prepare" the initial Sdl specication for a more accurate state space analysis. It consisted in basic static analysis techniques like dead code elimination and live variable detection using if2if. The bene ts were really spectacular on this example, and, in particular, the amount of memory required to store a model state fell to 0.2 kB. Finally, these optimisations made possible the use of exhaustive simulation techniques. More precisely we considered a system consisting in a pair of entities, communicating through a bounded fo channel, and we concentrated our validation e ort to a set of representative distinct scenarios (connection establishment, disconnection, data transfer, : : : ). Using speci c slicing criteria, it was therefore possible to (automatically) simplify even more the speci cation, depending on the property under veri cation or the test purpose. The underlying models obtained were about 20 000 states large, and errors were found in the data transfer phase of the speci cation. The complete experiment is reported in 9].

Mascara Protocol

The Mascara(Mobile Access Scheme based on Contention And Reservation for Atm) protocol is a special medium access control protocol designed for wireless Atm communication and developed by the wand(Wireless Atm Network Demonstrator) consortium 13]. A wireless Atm network extends transparently services to mobile terminals (mt) via a number of geographically distributed access points (ap). The task of the Mascara protocol is to mediate between aps and mts via a wireless link. The protocol has a layered structure, where we consider only the highest layer, the Mascara control layer. The overall description of the Mascara protocol which we got is 300 pages of Sdl textual code. We concentrate on the veri cation of the Mascara control layer, for which the Sdl description could be made reasonably complete. Here we brie y present the veri cation of the dynamic control. For complete information, we refer the reader to 17] which reports the complete experiment on the dynamic part. In addition, another veri cation experiment has been carried out on static control 4]. Veri cation should be carried out under a general environment with realistic restrictions. As we have not obtained information on the Mascara upper layer, we considered initially an open system with an unconstrained upper layer, which would allow us to obtain the most general veri cation results. But communication via unbounded channels, leads to in nitely growing channel contents and thus an in nite state model in case that the environment sends requests too often. This is typically the case in reactive systems always ready to treat requests from the environment. The approach we have chosen to provide a more restricted, but still realistic environment consists in limiting the number of requests it can make per time unit. We assume that within one time unit, no more than N requests can be sent by the environment. The system has never to deal with more than N requests simultaneously which leads, in the Mascara protocol, to bounded channel contents. The success of the method depends on the use of a realistic bound. We use N=4. Unfortunately, even with such a restricted environment, it was impossible to generate the state graph of the global system as a whole. However, we have applied two di erent types of compositional veri cation: the rst one is based on property decomposition 26], and the second one is based on compositional generation of a state graph minimized with respect to a behavioral equivalence 18]. In particular, using in addition both live analysis and partial order reduction for the generation of the subsystems, we were able to compositionally generate a reduced model of the global system using compositional generation. Table 4.2 gives an overview of a subset of the models we have generated using different reduction techniques and allows to compare their sizes and generation times. Finally, several properties ranging for generic ones such as deadlocks and livelocks to more speci c such as association establishment, connection, disconnection, were veri ed on the generated models.

Ariane-5 Flight Program

The work on this experiment was initiated by Eads Launch Vehicles to better evaluate the applicability of formal validation techniques on an existing software, the Ariane-51 Flight Program. This is the embedded software which solely controls the Ariane-5 launcher during its ight, from the ground, through the atmosphere and up to the nal orbit. The veri cation experiment is reported in 11]. First, this software has been formally speci ed in Sdl by reverse engineering from the existing code. Then, following a set of general methodological guidelines, the speci cation has been continuously improved and all the initial requirements were veri ed on the nal version. In particular, the combination of di erent optimisation techniques, operating either at the source level (like static analysis or slicing) or at the semantic level (like partialorder reductions) happened to be particularly useful in order to deal with large size state spaces. For example, the initial Sdl version of the ight program used no less than 130 timers. Using our static analysis tool we were able to reduce them to only 55 timers, functionally independent ones. Afterward, the whole speci cation was rewritten taking into account the redundancies discovered by the analyzer. The main di culty of this case-study comes from the combination of various kind of time constraints. On one hand, the functionality of the ight program strongly depends on an absolute time: coordination dates are frequently exchanged between components in order to synchronise their behaviour during the whole ight. On the other hand, this system has to be veri ed within a partially constrained environment, reacting with some degree of temporal uncertainty. In this experiment, this expressivity problem was solved at the IF level thanks to explicit urgency attributes. Clearly, such features should be made available at speci cation level. In particular, ongoing work address the introduction of high-level time and performance annotations in Sdl 10]. In practice, we have considered two di erent situations regarding the environment. The rst one is time-deterministic, which means that all environment actions (in particular the control part) take place at precise moments in time. The second one is time-nondeterministic which means that environment actions take place with some degree of time uncertainty (within a prede ned time interval). From the environment point of view, the later situation corresponds to a whole set of scenarios, whereas the former situation focus only on a single one. Table 2 Several directions can be investigated to improve this environment. The rst direction of improvement concerns the IF language. As currently de ned, it allows only the description of static systems, were the number of components (processes and bu ers) as well as their interactions are xed throughout the execution. This strongly limits our ability to handle complex dynamic speci cations. We work on a less restrictive de nition, were both parameterized descriptions (containing some xed number of replicated components) as well as general dynamic creation and destruction of components are allowed. Furthermore, some improvements will be made regarding the description of components itself, such as the possibility to express structured control using composed states (like in statecharts).

A second direction of improvement concerns the IF simulator, the core component allowing to construct and to explore the underlying semantic model of IF specications. Currently, this model is labeled transition systems, and its construction and exploration are quite restricted: rst, only pure asynchronous execution (by interleaving) is possible and second, no access is provided to the state of the system (e.g, current values of variables, current states of processes). We envisage to improve these points, by implementing a exible simulator able, for instance, to deal with both synchronous and synchronous components, or more generally, to take into account some scheduling policy over components during the simulation. In addition, this simulator will interact with running components through a well-de ned abstract interface, thus allowing to integrate also external components (for example, directly expressed as executable code). A third direction of improvement concerns the validation methods. Clearly, we will continue to adapt and to improve our static analysers as well as our model checkers to handle the extended IF descriptions. Also, some work must be done to reduce the manual overhead, yet important, needed by sophisticated techniques such as compositional veri cation. Finally, another important issue concerns the validation of non-functional requirements. In particular, performance evaluation becomes crucial for an important part of internet protocols (such as Pgm or Rmtp-ii) which are not necessarily designed to achieve full reliability, but only an average correct behaviour with respect to probabilistic assumptions on their execution environment (e.g, propagation delays, message loss, network elements speed, etc). At middle term, we plan to connect to IF environment to simulation environments like Opnet

Fig. 1 .

 1 Fig. 1. An open validation environment for IF

  29] and Ses/Workbench 21]. The IF package can be downloaded at http://www-verimag.imag.fr/DIST SYS/IF.

  . A second transformation is based on the slicing technique 33]. It allows to automatically abstract a given speci cation by eliminating some irrelevant parts w.r.t. a given property or test purpose 7].

if2pml 4] is a tool developed at Eindhoven TU to translate IF speci cations into Promela.

The semantic model level components. Cadp 14] is a toolset for the veri cation of Lotos speci cations. It is developed by the Vasy team of Inria Rhône-Alpes and Verimag. Two of its model-checkers are connected to the IF environment: Aldebaran (bisimulation based), and Evaluator (alternating-free -calculus). For both tools, diagnostic sequences are computed on the Lts level and they can be translated back into Msc to be observed at the speci cation level. Kronos 34] is a model-checker for symbolic veri cation of Tctl formulae on communicating timed automata. The current connection with the IF environment is as follows: control states and discrete variables are expressed using the implicit enumerative representation, whereas clocks are expressed using a symbolic representation (particular polyhedra). Tgv 15] is a test sequence generator for conformance testing of distributed systems (joint work between Verimag and the Pampa project of Irisa). Test cases are computed during the exploration of the model and they are selected by means of test purposes.

Table 1 .

 1 Mascara veri cation results

	generation strategy	ap model time size	mt model time size	ap + mt model size
	-live reduction 7 308 400 st. 207 0 35 00 4 388 765 st. 171 0 58 00 -partial order 30 689 244 tr. 12 811 961 tr. + live reduction 351 202 st. 12 0 22 00 63 628 st. 1 0 03 00 -partial order 1 536 699 tr. 325 312 tr. + live reduction 28 069 st. 1 0 53 00 6 580 st. 7 00 218 130 st. + partial order 52 983 tr. 20 913 tr. 1 142 215 tr. + live reduction 1 630 st. 9 00 977 st. 3 00 + partial order 2 885 tr. 2 845 tr. + slicing

Table 2 .

 2 presents the sizes of both models generated according to di erent generation strategies. It gives also the average time required for verifying each kind of property (by temporal logic model checking and model minimisation respectively). Ariane-5 Flight Program veri cation results.5 Conclusion and PerspectivesThe IF environment has already been used to analyze some representative Sdl speci cations such as Sscop, an Atm signalisation protocol, Mascara, an Atm wireless transport protocol and Ariane-5 ight program, a part of the embedded software of Ariane-5 launchers. It is currently used in several on going industrial case-studies, including respectively real-time multicast protocols Pgm and Rmtp-ii, and the session initiation protocol Sip. The bene ts of combining several techniques, working at di erent program level, were clearly demonstrated. In particular, traditional model-checking techniques were not su cient to complete on these large size examples.

			time deterministic non-deterministic time
	-live reduction -partial order model + live reduction 2 201 760 st. na generation -partial order 18 706 871 tr. + live reduction 1 604 st. + partial order 1 642 tr.	na na 195 718 st. 278 263 tr.
	model veri cation	model minimisation model checking	1 00 15 00	20 00 2 0 00 00

Ariane-5 is an European Space Agency Project delegated to CNES France.

Acknowledgements

We gratefully thank Guoping Jia and Lucian Ghirvu for their help on tools development and experimentations.