David Delmas
email: david.delmas@airbus.com

Antoine Miné
email: antoine.mine@lip6.fr

Analysis of Software Patches Using Numerical Abstract Interpretation

whether they are published or not. The documents may come

Introduction

The problem of proving the functional equivalence of programs, or program parts, is fundamental [START_REF] Floyd | Assigning meanings to programs[END_REF]. It aims at comparing the behaviors of two programs running in the same environment, i.e. their input-output relationships. In this paper, we describe a static analysis which aims at inferring that two syntactically close versions of a program compute equal outputs, when run on equal inputs.

The main application of this analysis is regression verification [START_REF] Godlin | Regression verification[END_REF]: prove that a program change does not add any undesirable behavior. Take, for instance, the /* Like fstatat, but cache the result. If ST->st_size is -1, the status has not been gotten yet. If less than -1, fstatat failed with errno == -1 -ST->st_size. Otherwise, the status has already commit shown on Fig. 1, extracted from a revision control repository of the GNU core utilities. It describes a change in a library implementing core functions for removing files and directories, and used by the POSIX rm command. The main function of this library uses the POSIX fstatat function to read information on the file to delete. As the same status information is needed in several contexts, the library implements a caching mechanism. At initialization, the main function calls a cache stat init function, which initializes the st size field of the stat structure * st to -1. Then, it calls the cache fstatat function shown on Fig. 1 repeatedly, whenever status information is needed. Indeed, cache fstatat caches the results of the fstatat function. In revision v6.10 of Coreutils, this function used the st size field of the stat structure * st to store information on the error value returned by fstatat upon the first call. It did it in a way that ensures that st size <0 whenever errno>0, so as to use the sign of st size upon subsequent calls, to distinguish between successful and erroneous executions. This scheme works for operating systems where errno is always set to positive values. However, some systems, such as BeOS [START_REF]The Be Book[END_REF] and Haiku [START_REF]The Haiku Operating System[END_REF], allow for negative errno values. The fix displayed on Fig. 1 aims at accommodating such systems. It consists in storing errno directly in the st ino field of the stat structure.

On this example, non regression verification amounts to proving that the behavior of the main function of the library is unchanged on systems with only positive error values. This is, indeed, validated by our analysis. The analyzed source code includes a stub variable for errno, and stub code for the fstatat function. The stub for fstatat updates errno with a non-deterministic value, ranging over positive integers. Note that a separate analysis of the cache fstatat function, as opposed to an analysis of the whole library, makes it necessary to model its possible execution environments with an unbounded loop, calling cache fstatat an arbitrary number of times, with parameters taken from an arbitrary sequence of file names and stat structures. This unbounded sequence is modeled, in practice, using an unbounded number of reads from an input stream. Fig. 2 shows an example for n files, where n may be unbounded.

More generally, we are interested in analyzing patches of programs reading an unbounded number of input values, e.g. programs reading from file or I/O streams, and embedded reactive software with internal state, which no related work addresses. Or goal is to prove that the original and patched versions of such programs compute equal outputs, when run with the same sequence of inputs. We therefore model streams directly in the semantics on which our analysis is based (see section 1).

Running example

In the following, we sketch our approach to the analysis of semantic differences between two syntactically similar programs P 1 and P 2 . We are interested in proving that P 1 and P 2 compute equal outputs when run on equal inputs. P 1 and P 2 are represented together in the syntax of a so-called double program P . Simple programs P 1 and P 2 are referred to as the left and right projections of P . Fig. 3 shows the Unchloop example, taken from [START_REF] Trostanetski | Modular demand-driven analysis of semantic difference for program versions[END_REF], and translated into our syntax of double programs. The symbol is used to represent syntactic difference. It is available at expression, condition, and statement levels in our syntax for double programs. For instance at line 3, c ← 1 0 means c ← 1 for P 1 , and c ← 0 for P 2 . In contrast, line 4 means i ← 0 for both P 1 and P 2 . Let us describe the example program. Both versions P 1 and P 2 read inputs in the range [-1000, 1000] into a and b at lines 1 and 2. At line 3, the counter c is being initialised with value 1 for program P 1 , and value 0 for program P 2 . Then, both programs add a times the value of b to c in a loop. Finally, they both store the result into r at line 9: c for P 1 , c+1 for P 2 . The assertion at line 10 expresses the property we would like to check: if both programs reach it, then they should have computed equal values for r.

We assume here that both programs read the same input value in a, and the same input value in b. More generally, the semantics of P is parameterized by a (possibly infinite) sequence of input values, and we wish to prove that, given the same sequence of input values, P 1 and P 2 have the same result in r.

1 : a ← input(-1000, 1000); 2 : b ← input(-1000, 1000); 3 : c ← 1 0; 4 : i ← 0; 5 : while (i < a) { 6 :

c ← c + b; 7 :

i ← i + 1; 8 : } 9 : r ← c c + 1; 10 : assert sync(r); Fig. 3. Unchloop example

1 : x ← input(-100, 100); 2 : if (x < 0) x ← -1; 3 : else { 4 : if (x ≥ 2 x ≥ 4) {} // x > 4 in original paper 5 :
else { 6 :

while (i = 2) x ← 2; 7 :

x ← 3; 8 : } 9 : } 10 : assert sync(x); // x = 2 ignored Fig. 4. Modified [24, Fig. 2

] example

The assertion at line 10 of our example is thus valid. It is, indeed, validated by our analysis.

Limitations Our analysis is based on abstractions of a concrete collecting semantics which will be presented in section 1. This semantics relates pairs of terminating executions of projections of a double program. It is suitable to prove a number of properties, including that two terminating programs starting from equal initial states will produce equal outputs, a notion called partial equivalence in [START_REF] Godlin | Regression verification[END_REF]. In contrast, an analysis based on this collecting semantics will fail to report differences between pairs of executions where at least one of the programs does not terminate. For instance, in the example on Fig. 4, our analysis does not report any difference between P 1 and P 2 , although P 1 terminates on input x = 2, and P 2 does not.

As opposed to [START_REF] Partush | Abstract semantic differencing for numerical programs[END_REF][START_REF] Partush | Abstract semantic differencing via speculative correlation[END_REF], which develop algorithms to automate the construction of a correlating program P 1 P 2 , on which to run the static analysis, we assume for now the joint representation of P 1 and P 2 given, as part of a double program in our toy language.

Related work [START_REF] Jackson | Semantic diff: A tool for summarizing the effects of modifications[END_REF] pioneered the field of semantic differencing between two versions of a procedure by comparing dependencies between input and output variables. Symbolic execution methods [START_REF] Person | Differential symbolic execution[END_REF][START_REF] Trostanetski | Modular demand-driven analysis of semantic difference for program versions[END_REF][START_REF] Mora | Client-specific equivalence checking[END_REF] have proposed analysis techniques for programs with small state space and bounded loops, which may support modular regression verification. On the contrary, we can handle programs with unbounded loops and an infinite number of execution paths, like the example of Figs. 1 and2. Some approaches [START_REF] Marinescu | Katch: High-coverage testing of software patches[END_REF] combine symbolic execution and program analysis techniques to improve the coverage of patches with tests suites, but such testing coverage criteria bring no formal guarantee of correctness, unlike our method.

RVT [START_REF] Godlin | Regression verification[END_REF] and SymDiff [START_REF] Lahiri | Symdiff: A languageagnostic semantic diff tool for imperative programs[END_REF][START_REF] Lahiri | Differential assertion checking[END_REF] combine two versions of the same program, with equality constraints on their inputs, and compile equivalence properties into verification conditions to be checked by SMT solvers. On the contrary, we rely on abstract domains to infer equivalence properties.

The DIZY [START_REF] Partush | Abstract semantic differencing for numerical programs[END_REF][START_REF] Partush | Abstract semantic differencing via speculative correlation[END_REF] tool leverages numerical abstract interpretation to establish equivalence under abstraction. In particular, the authors give a semi-formal description of an operational concrete trace semantics. This semantics is not defined by induction on the syntax, and does not support streams. Our main contribution, with respect to this work, is a novel, fully formalized, denotational concrete collecting semantics by induction on the syntax, which can deal with programs reading from infinite input streams, and a novel numeric domain to bound differences between the values of the variables in the two programs. Another difference is that [START_REF] Partush | Abstract semantic differencing for numerical programs[END_REF][START_REF] Partush | Abstract semantic differencing via speculative correlation[END_REF] rely on program transformations to build a correlating program, which they analyze according to simple program semantics, while our semantics is defined for double programs directly.

The Fluctuat [START_REF] Martel | Propagation of roundoff errors in finite precision computations: A semantics approach[END_REF][START_REF] Goubault | Static analysis of finite precision computations[END_REF] static analyser compares the real and floating-point semantics of numeric programs to bound errors in floating-point computations. The authors use the zonotope abstract domain to bound the difference between real and floating-point values. Like in our concrete semantics, they also address unstable test analysis [START_REF] Goubault | Robustness analysis of finite precision implementations[END_REF].

Contributions The main contributions of this work are:

-We present a novel concrete collecting semantics, expressing the behaviors of two versions of a program at the same time. This semantics deals with programs reading from unbounded input streams. -We propose an abstraction of infinite input streams able to prove that programs that read from the same stream compute equal output values. -We introduce a novel numeric domain to bound differences between the values of the variables in the two programs, which has linear cost, and the right amount of relationality to express useful properties of software patches. -We implemented a prototype static analyzer which exhibits significant speedups with respect to previous works.

We build on previous work [START_REF] Delmas | Analysis of Program Differences with Numerical Abstract Interpretation[END_REF]. The main contributions of the current paper, with respect to this work, is a formal treatment of infinite input streams, in the concrete and abstract semantics.

The paper is organised as follows. Section 1 formalizes the concrete collecting semantics, and illustrates it on the example from Fig. 3. Section 2 describes

stat ::= V ← expr V ∈ V | V ← input(a, b) a, b ∈ R | if cond then stat else stat | while cond do stat | stat; stat | skip (a) Simple statements expr ::= V V ∈ V | c c ∈ R | -expr | expr expr ∈ {+, -, ×, /} | rand(a, b) a, b ∈ R cond ::= expr expr ∈ {≤, ≥, =, =, <, >} | ¬cond | cond cond ∈ {∧, ∨} (b)
Simple expressions and conditions the abstract semantics, discusses the choice of numeric abstract domains, and introduces a novel numeric domain. Section 3 presents experimental results with a prototype implementation. Section 4 concludes.

dstat ::= stat | stat stat | V ← dexpr V ∈ V | assert sync(V ) | dstat; dstat | if dcond then dstat else dstat | while dcond do dstat

Syntax and concrete semantics

Following the standard approach to abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], we developed a concrete collecting semantics for a toy While language for double programs. The operator may occur anywhere in the parse tree, to denote syntactic differences between the left and right projections of a double program. However, operators cannot be nested: a double program only describes a pair of programs.

Given double program P with variables in V, consider its left (resp. right) projection P 1 = π 1 (P ) (resp. P 2 = π 2 (P )), where π 1 (resp. π 2 ) is a projection operator defined by induction on the syntax, keeping only the left (resp. right) side of symbols. For instance,

π 1 (c ← 1 0) = c ← 1, and π 2 (c ← 1 0) = c ← 0, while π 1 (i ← 0) = i ← 0 = π 2 (i ← 0).
1.1 Simple programs P 1 and P 2 are simple programs, with concrete memory states in E V → R. Let k ∈ {1; 2}. The syntax of simple program P k is standard. Statements stat are presented in Fig. 5(a). They are built on top of numeric expressions expr and Boolean conditions cond , defined in Fig. 5(b). To define the semantics of simple program P k , we leverage standard, relational, input-output semantics, defined by induction on the syntax, in denotational style. Given E e ∈ E → P(R) for non-deterministic expression e ∈ expr , and C c ∈ E → P({true, false}) for condition c ∈ cond , we let S s describe the relation between input and output states of statement s ∈ stat. Because of the input command, which reads some input stream, S s is parameterised by a sequence of values, and program states record the current index in this sequence. Note that this sequence has to be infinite: indeed, due to non-determinism, the concrete semantics maps every input stream to a (possibly infinite) set of executions, which can execute an unbounded number of input statements. Therefore S s ∈ R ω → P(E × E ),

where E E × N, and:

S V ← input(a, b) σ { ((ρ, n), (ρ[V → σ n ], n + 1)) | (ρ, n) ∈ E ∧ a ≤ σ n ≤ b }
Note that we model one input stream only, but the generalization to several input streams is obvious. We do not display the semantics for other commands, as the semantics for assignments and tests are standard for memory environments, and leave indexes unchanged. For instance,

S V ← e σ { ((ρ, n), (ρ[V → v], n)) | (ρ, n) ∈ E ∧ v ∈ E e ρ }.

Double programs

We then lift the semantics S to double programs. As P 1 and P 2 have concrete states in E , P has concrete states in D E × E . The syntax of double statements dstat is shown in Fig. 5(c). They are built on top of double expressions dexpr and double conditions dcond , defined in Fig. 5(d

relations: R 1 R 2 { (x, z) | ∃y : (x, y) ∈ R 1 ∧ (y, z) ∈ R 2 }.
The semantics for assignments of double expressions D V ← e 1 e 2 (different expressions to the same variable) is defined using this construct. The interest of double expressions in the syntax is to allow for simple symbolic simplifications in later abstraction steps, when computing differences between expressions assigned to a variable. The semantics of assert sync(V ) statements asserts that the left and right projections of a double program agree on the value of variable V . The semantics for the sequential composition of statements boils down to the composition of the semantics of individual statements. The semantics for selection statements relies on the filter F c 1 c 2 to distinguish between cases where both projections agree on the value of the controlling expression, and cases where they do not (a.k.a. unstable tests). There are two stable and two unstable test cases, according to the evaluations of the two conditions. The semantics for stable test cases is standard. The semantics for unstable test cases is defined by composing the left Note that the semantics D V ← input(a, b) of input statements is different from the semantics D V ← rand(a, b) of non-deterministic assignments. The latter entails no relationship between the values read by the two projections of a double program, besides the fact that they range in the same interval. On the contrary, the former reads from a shared input stream σ, hence the left and right projections P 1 and P 2 read equal values if their input indexes n 1 and n 2 are equal. This is the case when P 1 and P 2 have called input equal numbers of times. On the contrary, if one projection, say P 1 , has called input more often than the other, then P 1 is ahead of P 2 in the stream, and the two projections are desynchronized. Nonetheless, they may resynchronize later if P 2 catches up with P 1 , hence read equal values again. Also, owing to the semantics to read the input at the same index. For the sake of simplicity, we do not check this in our semantics (altough our implementation performs this check).

D dstat ∈ R ω → P(D × D ) D skip σ ∆ D D s1 s2 σ { ((i1, i2), (o1, o2)) | (i1, o1) ∈ S s1 σ ∧ (i2, o2) ∈ S s2 σ } D V ← e1 e2 σ D V ← e1 V ← e2 σ D V ← e σ D V ← e V ← e σ D V ← input(a, b) σ D V ← input(a, b) V ← input(a, b) σ D assert sync(V ) σ { (((ρ1, n1), (ρ2, n2)), ((ρ1, n1), (ρ2, n2))) | ρ1(V ) = ρ2(V ) } D s ; t σ D s σ D t σ D if c1 c2 then s else t σ F c1 c2 D s σ ∪ F c1 ¬c2 D π1(s) skip σ D skip π2(t) σ ∪ F ¬c1 c2 D π1(t) skip σ D skip π2(s) σ ∪ F ¬c1 ¬c2 D t σ D if c then s else t σ D if c c then s else t σ D while c1 c2 do s σ (lfp H) F ¬c1 ¬c2 D while c do s σ D while c c do s σ where F c1 c2 { (((ρ1, n1), (ρ2, n2)), ((ρ1, n1), (ρ2, n2))) | true ∈ C c1 ρ1 ∩ C c2 ρ2 } and H(R) ∆ D ∪ R F c1 c2 D s σ ∪ F c1 ¬c2 D π1(s) skip σ ∪ F ¬c1 c2 D skip π2(s) σ
The presence of both input and rand primitives makes the semantics very expressive, and useful for modeling many practical problems. Non-determinism allows to abstract unknown parts of a program: for instance, rand(0, 10) is a sound stub for f (), when function f is only known to return values between 0 and 10. Also, combining input and rand allows to model information flow

Properties of interest

We wish to prove the functional equivalence of the left and right projections of a given double program P ∈ dstat, restricted to a set of distinguished variables V 0 ∈ P(V), specified with the assert sync primitive. Let I 0 {((λV. 0, 0), (λV. 0, 0))} be the singleton state with all variables and input indexes initialized to zero. The set of states reachable by P from I 0 with input stream σ is (D P σ)I 0 . Therefore the property of interest may be formalized as:

∀σ ∈ R ω : ∀V ∈ V 0 : ∀((ρ 1 , n 1 ), (ρ 2 , n 2 )) ∈ (D P σ)I 0 : ρ 1 (V ) = ρ 2 (V )
Coming back to our running example Unchloop on Fig. 3, the concrete semantics of the program from line 3 to 9 is displayed on Fig. 7, for any sequence of inputs σ ∈ R ω . With the additional assumption that both program projections compute with equal inputs (a

1 = a 2 = σ 0 ∧ b 1 = b 2 = σ 1 )
, ensured by the semantics of line 1 and 2, and the initial environment I 0 , the two projections can be proved to compute equal values for r. D U nchloop3..9 σ = { s0, ((a1, b1, 1, 0, 1, n1), (a2, b2, 0, 0, 1, n2))

| a1 ≤ 0 ∧ a2 ≤ ∧ H0 } ∪ { s0, ((a1, b1, 1 + a1 × b1, a1, 1 + a1 × b1, n1), (a2, b2, 0, 0, 1, n2)) | a1 > 0 ∧ a2 ≤ ∧ H0 } ∪ { s0, ((a1, b1, 1, 0, 1, n1), (a2, b2, a2 × b2, a2, 1 + a2 × b2, n2)) | a1 ≤ 0 ∧ a2 > ∧ H0 } ∪ { s0, ((a1, b1, 1 + a1 × b1, a1, 1 + a1 × b1, n1), (a2, b2, a2 × b2, a2, 1 + a2 × b2, n2)) | a1 > 0 ∧ a2 > ∧ H0 } where s0 ((a k , b k , c k , i k , r k ), n k ) k∈{1,2}
and H0 s0 ∈ R 4 × N Fig. 7. Concrete semantics of the Unchloop example from Fig. 3 Unfortunately, our concrete collecting semantics D is not computable in general. A particular difficulty of the Unchloop example is that the input-ouptut relation is non linear: (a ≤ 0 ⇒ r = 1) ∧ (a ≥ 0 ⇒ r = 1 + a × b). Hence, inferring such information is beyond classic numeric domains, such as polyhedra. We will provide a new analysis method which avoids resorting to more complex, non-linear numeric domains. An additional difficulty, not shown in the Unchloop example, is that the programs can read an unbounded number of values from their input stream.

(R ω → P(D × D ), ⊆) ----→ -→ ← ←----- α F γ F (P( D × D), ⊆) α F (f ) { (βσ(s), βσ(s )) | (s, s ) ∈ f (σ) ∧ σ ∈ R ω } (γ F (R))(σ) { (s, s ) | (βσ(s), βσ(s )) ∈ R } where ∀ σ ∈ R ω : βσ ∈ D → D βσ(((ρ1, n1), (ρ2, n2))) (ρ1, ρ2, δ, q) with δ = n2 -n1 ∧ |q| = |δ| ∧ ∀ 0 ≤ n < |δ| : qn = σ max{n 1 ,n 2 }-n-1
Fig. 8. Abstraction of shared input sequences with unbounded FIFO queues

Abstract semantics

We therefore tailor an abstract semantics suitable for the analysis of program differences.

Wrapping up infinite input sequences

A first observation is that we do not need to recall the whole input sequence σ ∈ R ω shared by the left and right projections P 1 and P 2 of a double program P . Indeed, we only aim at inferring equalities between the input values read by P 1 and P 2 . We therefore only need to record, at any point in the analysis, the input subsequence that has been read by one program, but not the other one yet. This ensures that, when a program that has read less values than the other catches up with it, it reads the same values. Values read by both programs can be discarded, and values not read by any program do not need to be known in advance, as they can be chosen non-deterministically. This subsequence of input values read by one program only forms an (unbounded) FIFO queue, as inputs are read in order. We therefore abstract the input sequence σ, and indexes n 1 and n 2 of P 1 and P 2 in this sequence, defined in D , as the difference δ n 2 -n 1 , and a FIFO queue of length |δ| in D E ×E ×Z×R . This abstraction does not lose information. A formalization of this abstraction is shown on Fig. 8. Note that we use the symbol ⊆ to denote the pointwise lifting of ⊆:

f ⊆f ≡ ∀σ ∈ R ω : f (σ) ⊆ f (σ).
Proposition 1. The pair (α F , γ F ) defined in Fig. 8 is a Galois isomorphism.

Note that this abstraction includes some redundancy: indeed, it would be enough to record only the sign of δ, instead of its value, as its absolute value is given by the length of the queue. However, keeping the value simplifies subsequent abstraction steps.

Simple programs Starting from the concrete semantics D, let us now formalize the semantics resulting from this first abstraction step. To start with, we first define the simple program semantics. The behaviors of the left and right projections P 1 and P 2 of a double program P depend on which is ahead in the input sequence, and which is behind. P 1 is ahead if δ < 0, and P 2 is 9. Abstract semantics of simple programs P1 and P2 with unbounded queues ahead if δ > 0. Therefore, we need to particularize the simple program semantics Ŝk s ∈ P( Ê × Ê), where Ê E × Z × R , and k ∈ {1, 2}. Fig. 9 shows the semantics for Ŝk V ← input(a, b) . Note that we write q • q to denote concatenation of queues q and q . Intuitively, this semantics distinguishes between two cases:

Ŝk s ∈ P( Ê × Ê) ; k ∈ {1, 2} Ŝ1 V ← input(a, b) { ((ρ, δ, q), (ρ[V → ν], δ -1, ν • q)) | (ρ, δ, q) ∈ Ê ∧ δ ≤ 0 ∧ a ≤ ν ≤ b } ∪ { ((ρ, δ, q • v), (ρ[V → v], δ -1, q)) | (ρ, δ, q) ∈ Ê ∧ δ > 0 ∧ a ≤ v ≤ b } Ŝ2 V ← input(a, b) { ((ρ, δ, q), (ρ[V → ν], δ + 1, ν • q)) | (ρ, δ, q) ∈ Ê ∧ δ ≥ 0 ∧ a ≤ ν ≤ b } ∪ { ((ρ, δ, q • v), (ρ[V → v], δ + 1, q)) | (ρ, δ, q) ∈ Ê ∧ δ < 0 ∧ a ≤ v ≤ b } Fig.
1. If program P k is ahead of the other program in the input sequence, or at the same point, then a new successful input read operation produces a fresh input value, and adds it at the head of the queue. 2. If program P k is behind the other program in the input sequence, then a new successful input read operation retrieves the value at the tail of the queue.

In both cases, an input read operation is only successful if the value read matches the bounds specified for the input statement. We do not display the semantics for other commands, as the semantics for assignments and tests are standard for memory environments, and leave input index differences and queues unchanged. For instance, Ŝk V ← e { ((ρ, δ, q), (ρ D1 s { ((ρ1, ρ2, δ, q), (ρ 1 , ρ2, δ , q )) | ((ρ1, δ, q), (ρ 1 , δ , q )) ∈ Ŝ1 s ∧ ρ2 ∈ E } D2 s { ((ρ1, ρ2, δ, q), (ρ1, ρ 2 , δ , q )) | ((ρ2, δ, q), (ρ 2 , δ , q

[V → v], δ, q)) | (ρ, δ, q) ∈ Ê ∧ v ∈ E e ρ }.

Double programs

)) ∈ Ŝ2 s ∧ ρ1 ∈ E } F c1 c2 F1 c1 F2 c2
Fk c { ((ρ1, ρ2, δ, q), (ρ1, ρ2, δ, q)) | (ρ1, ρ2, δ, q) ∈ D ∧ true ∈ C c ρ k } ; k ∈ {1; 2} Fig. 10. Abstract semantics of double programs with unbounded queues

(P( D × D), ⊆) ---→ -→ ← ----- αp γp (P( Dp × Dp), ⊆) αp(R) { (βp(s), βp(s )) | (s, s ) ∈ R } γp(R) { (s, s ) | (βp(s), βp(s )) ∈ R } where βp ∈ D → Dp βp((ρ1, ρ2, δ, q)) (ρ1, ρ2, δ, q) with qn = qn if 0 ≤ n < |δ| 0 if |δ| ≤ n < p

Bounding input queues

The abstract semantics D features unbounded queues. We aim at abstracting the concrete collecting semantics D in numeric domains, so we need to deal with a bounded number of variables. As it is also simpler to deal with a fixed number of variables, we parameterize our abstract semantics with some predetermined integer p ≥ 1, used to define the lengths of abstract FIFO queues in domain Dp In any case, an input read operation is only successful if the value read matches the bounds specified for the input statement. We do not display the semantics for other commands, as the semantics for assignments and tests are standard for memory environments, and leave input index differences and queues unchanged. For instance, Ŝp

E × E × Z × R p .
((ρ1, δ, q • v), (ρ1[V1 → ν], δ -1, ν • q)) (ρ1, δ, q) ∈ Ep-1 ∧ δ ≤ 0 ∧ a ≤ ν ≤ b ∧ v ∈ R ∪ ((ρ1, δ, q • v • r), (ρ1[V1 → v], δ -1, q • 0 • r)) (ρ1, δ, q) ∈ E |δ|-1 ∧ 0 < δ ≤ p ∧ a ≤ v ≤ b r ∈ R p-2 ∧ ∀ 0 ≤ n < p -2 : rn = 0 ∪ ((ρ1, δ, q), (ρ1[V1 → ν], δ -1, q)) (ρ1, δ, q) ∈ Ep ∧ δ > p ∧ a ≤ ν ≤ b Fig.
k V ← e { ((ρ, δ, q), (ρ[V → v], δ, q)) | (ρ, δ, q) ∈ E p ∧ v ∈ E e ρ }.

Double programs

We then lift the semantics Ŝp 1 s and Ŝp 2 s to double programs. The definition of Dp s ∈ P( Dp × Dp ) is very similar to that of D s . The main change is that Dp k s is defined with Ŝp k s , where Dk s is defined with Ŝk s . We thus only show the definitions of some relations on Fig. 13. These definitions are very similar to those of D s on Fig. 10. The semantics for double statements and conditions compose the semantics of their left and right projections. The order of the composition is arbitrary, but significant for statements, as Dp 1 s Dp 2 t = Dp 2 t Dp 1 s . Both composition orders, however, are sound. A way to make the analyse precise and independent on the order would be to compute the intersection of the compositions with the two orders. The order is in constrast not significant for conditions, as Fp { ((ρ1, ρ2, δ, q), (ρ 1 , ρ2, δ , q )) | ((ρ1, δ, q), (ρ 1 , δ , q )) ∈ Ŝp

1 s ∧ ρ2 ∈ E } Dp 2 s { ((ρ1, ρ2, δ, q), (ρ1, ρ 2 , δ , q )) | ((ρ2, δ, q), (ρ 2 , δ , q )) ∈ Ŝp 2 s ∧ ρ1 ∈ E } Fp c1 c2 Fp 1 c1 Fp 2 c2 Fp k c
{ ((ρ1, ρ2, δ, q), (ρ1, ρ2, δ, q)) | (ρ1, ρ2, δ, q) ∈ Dp ∧ true ∈ C c ρ k } ; k ∈ {1; 2} Fig. 13. Abstract semantics of double programs with queues of length p ≥ 1

Numerical abstraction

We now rely on numeric abstractions to abstract further Dp s into a computable abstract semantics D p s , resulting in an effective static analysis.

Connecting to numeric domains As Dp ≈ R 2|V|+p+1 , any numeric abstract domain with 2|V|+p+1 dimensions may be used, such as polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. Let N be such an abstract domain, with values in D , order , concretization γ N ∈ D → P(R 2|V|+p+1 ), and operators Ŝ p s , Ĉ p c ∈ D → D for assignments and tests of simple programs over variables in

V 1 ∪ V 2 ∪ Q, where V k { x k | x ∈ V }, and Q {δ, (q n ) 0≤n<p }.
Let ∪ and ∩ be the abstractions of set union and intersection of domain N , and be its widening operator. We abstract Dp s ∈ P( Dp × Dp ) by D p s ∈ D → D , with the soundness condition ∀X ∈ D : Dp s (γ N (X )) ⊆ γ N ( D p s (X )). As Dp s is defined by induction on the syntax, the definition for D p s is straightforward: the abstract semantics needs only be defined for the composition of syntactically different statements s 1 s 2 and conditions c 1 c 2 . Fig. 14 shows definitions for associate transfer functions, as well as the transfer functions for some of the other syntactic constructs. We use the syntactic renaming operator τ 1 (resp. τ 2 ), defined by induction on the syntax, to distinguish the variables of the left (resp. right) projection of a double program, with suffix 1 (resp. 2). For instance,

D p c ← 1 0 = Ŝ p c 2 ← 0 • Ŝ p c 1 ← 1 .
Leveraging standard numeric domains Coming back to the example Unchloop from Fig. 3, recall that the relation between c and i is non linear: c 1 = i 1 ×b 1 +1 and c 2 = i 2 × b 2 from line 4 to line 9. Thus, a separate analysis of programs P 1 and P 2 would require a non linear abstract domain to compare r 1 and r 2 . In contrast, our joint analysis of P 1 and P 2 will be sufficiently precise, even when using linear numeric domains, because the difference between the values of the variables in P 1 and in P 2 remains linear. For instance, the polyhedra domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] is able to infer that the invariant -c 1 + c 2 + 1 = 0 holds from line 3 to 9, hence r 1 = r 2 at line 9, although it is not able to discover any interval for r 1 or r 2 . The octagon domain [START_REF] Miné | The octagon abstract domain[END_REF] is also able to express these invariants, but its transfer function for assignment is not precise enough to infer them. Indeed, x ← a -b

D p s ∈ D → D D p s1 s2 D p 2 s2 • D p 1 s1 D p k s Ŝ p τ k (s) ; k ∈ {1; 2} F p c1 c2 F p 2 c2 • F p 1 c1 F p k c Ĉ p τ k (c) ; k ∈ {1; 2} D p V ← e1 e2 Ŝ p V2 ← τ2(e2) • Ŝ p V1 ← τ1(e1) D p 1 V ← input(a, b) Ŝ p δ ← δ -1 • Ŝ p V1 ← q0 • Ŝ p q0 ← rand(a, b) • Ŝ p q1 ← q0 • • • • • Ŝ p qp-1 ← qp-2 • Ĉ p δ ≤ 0 ∪ Ŝ p q δ-1 ← 0 • Ŝ p V1 ← q δ-1 • Ĉ p q δ-1 ≤ b • Ĉ p q δ-1 ≥ a • Ĉ p δ ≤ p • Ĉ p δ > 0 ∪ Ŝ p V1 ← rand(a, b) • Ĉ p δ > p D p 2 V ← input(a, b) Ŝ p δ ← δ + 1 • Ŝ p V2 ← q0 • Ŝ p q0 ← rand(a, b) • Ŝ p q1 ← q0 • • • • • Ŝ p qp-1 ← qp-2 • Ĉ p δ ≥ 0 ∪ Ŝ p q -δ-1 ← 0 • Ŝ p V2 ← q -δ-1 • Ĉ p q -δ-1 ≤ b • Ĉ p q -δ-1 ≥ a • Ĉ p δ ≥ -p • Ĉ p δ < 0 ∪ Ŝ p V2 ← rand(a, b) • Ĉ p δ < -p where τ k (x) x k if x ∈ V x if x ∈ Q Fig. 14.
Abstract semantics of double programs with a standard numeric domain 15. Abstraction of double environments with environment differences cannot be exactly abstracted by the domain, and currently proposed transfer functions fall back to plain interval arithmetics in that case, so that the domain cannot exploit the bound it infers on a -b to bound x, for efficiency reasons. The interval domain is not able to express the invariants, hence it cannot be used directly for a conclusive analysis.

(P( Dp × Dp), ⊆) ----→ -→ ← ←----- α - γ - (P( Dp × Dp), ⊆) α-(R) ((ρ1, ρ2 -ρ1, δ , q), (ρ 1 , ρ 2 -ρ 1 , δ , q )) ((ρ1, ρ2, δ , q), (ρ 1 , ρ 2 , δ , q )) ∈ R γ-(∆) ((ρ1, ρ1 + δρ, δ , q), (ρ 1 , ρ 1 + δ ρ , δ , q )) ((ρ1, δρ, δ , q), (ρ 1 , δ ρ , δ , q )) ∈ ∆ Fig.

Introducing a dedicated numeric domain

However, we remark that it is sufficient to bound the difference x 2 -x 1 for any variable x to express the necessary invariants, where x 1 (resp. x 2 ) represents the value of x for the left (resp. right) projection P 1 (resp. P 2 ) of a double program P . Thus, we now design an abstract domain that is specialized to infer these bounds.

We abstract the values x 1 and x 2 by the pair (x 1 , δx), where δx x 2 -x 1 . This abstraction amounts to changing the representation of states of double program P . It does not lose information. A formalization of this abstraction is shown on Fig. 15. Note that we extend operators + and -to functions (pointwise lifting).

Proposition 5. The pair (α -, γ -) defined in Fig. 15 is a Galois isomorphism.

Let p α -( Dp ). p is able to represent two-variable equalities x 1 = x 2 ⇔ δx = 0, even after numeric abstraction using non relational domains, such as For instance, after statement a ← input(-1000, 1000) at line 1 of the Unchloop example on Fig. 3, we have a ∈ [-1000, 1000], and δa = 0. The second particular case is that of affine assignments V ← e, where e = µ + x∈V λ x × x. We call such expressions "differentiable", as it is easy to compute δV directly as a function of all the δx variables. A third particular case is that of arbitrary (non necessarily affine) assignments V ← e, when e is deterministic, and all the occurring variables x satisfy δx = 0. Then δV = 0, as we know that both expressions always evaluate to equal values in P 1 and P 2 .

To further enhance precision on some examples, we slightly generalize these particular cases to double assignments V ← e 1 e 2 , when expressions e 1 and e 2 are found syntactically equal, modulo some semantics preserving transformations, such as associativity, commutativity, and distributivity. We also generalize symbolic simplifications based on expression differentation to some double assignments V ← e e + e , in particular when e is a constant. For instance, for line 9 of the Unchloop example on Fig. 3, we have p

2 r ← c c + 1 = Ŝ p δr ← δc + 1 .
As a consequence, the interval domain is able to infer the invariant δr = 0 for semantics p at line 10 of this example, resulting a conclusive analysis with linear cost, which is much more efficient than using polyhedra with D p .

Evaluation

We implemented a prototype abstract interpreter for the semantics D p and p of the toy language introduced in this paper. It is about 2,500 lines of OCaml source code. It uses the Apron [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF] library to experiment with the polyhedra and octagon abstract domains, and the BddApron [START_REF] Jeannet | Bddapron: A logico-numerical abstract domain library[END_REF] library to implement state partitioning.

Benchmarking

We compare results on small examples selected from other authors' benchmarks [START_REF] Trostanetski | Modular demand-driven analysis of semantic difference for program versions[END_REF][START_REF] Partush | Abstract semantic differencing for numerical programs[END_REF][START_REF] Partush | Abstract semantic differencing via speculative correlation[END_REF]. Note that some of these benchmarks originate from real patches in GNU core utilities. We added a larger benchmark (also from a Coreutils patch), to evaluate scalability. For most benchmarks, patches preserve most of the loop and branching structure, except for the seq benchmark from [START_REF] Partush | Abstract semantic differencing for numerical programs[END_REF][START_REF] Partush | Abstract semantic differencing via speculative correlation[END_REF], which features deep modifications of the control structure. The related works do not address streams. As a consequence, these benchmarks do not feature unbounded reads into input streams, except for the remove benchmark, which we presented in the introduction: see Fig. 1 and Fig. 2. Note that we simplified this benchmark to fstatat caching for a single file, in order to compare with [START_REF] Partush | Abstract semantic differencing for numerical programs[END_REF]. [START_REF] Trostanetski | Modular demand-driven analysis of semantic difference for program versions[END_REF][START_REF] Partush | Abstract semantic differencing for numerical programs[END_REF][START_REF] Partush | Abstract semantic differencing via speculative correlation[END_REF] deal with C programs directly, while we encode their benchmarks in our toy language. In addition, these references not only prove equivalences, but also characterize differences, while we focus on equivalence for now. We therefore selected benchmarks relevant to equivalence only, except for the [24, Fig. 2] example, which we modified slightly to restore equivalence of terminating executions: see Fig. 4. On the other hand, [START_REF] Trostanetski | Modular demand-driven analysis of semantic difference for program versions[END_REF] gives several versions of their benchmarks, depending on the maximum numbers of loop iterations of the examples. Indeed, the symbolic execution technique they use is very sensitive to this parameter. We do not have this constraint, as we use widening instead of fully unrolling loops, so that we handle directly unbounded loops in a sound way.

Figure 18 summarises the results of our analysis. It shows the analysis timings and results of our prototype, as well as timings of the analyses the related work, when they are available (their analyses are all successful). All experiments were conducted on a Intel R Core-i7 TM processor. Our results are comparable with those of the original authors, with speedups of one order of magnitude or more. Some timing differences, of the order of milliseconds, cannot be considered significant, especially as the experiments are not performed on the same machines. A significant point, however, is that the benchmark LoopMult takes 49 seconds in [START_REF] Trostanetski | Modular demand-driven analysis of semantic difference for program versions[END_REF], which is two orders of magnitude slower than the benchmark Const, while, with our method, both Const and LoopMult are analyzed at roughly the same speed. This difference in behaviors can be explained as a benefit of widening over unrolling loops. Hence, our timing comparison proves that our method can achieve at worst a similar speed, and it is also much more scalable for problems difficult in previous work. Note that [START_REF] Trostanetski | Modular demand-driven analysis of semantic difference for program versions[END_REF] compared their method to well-established tools, such as Symdiff [START_REF] Lahiri | Symdiff: A languageagnostic semantic diff tool for imperative programs[END_REF] and RVT [START_REF] Godlin | Regression verification[END_REF], and observed speedups of one order of magnitude and more with respect to them. Therefore, it is not useful to compare our prototype with these tools on these benchmarks.

Most benchmarks are analyzed successfully with the polyhedra domain, without partitioning. The seq benchmark, for instance, is analyzed precisely despite significant changes in the control structure, as the matching of statements is established as part of the syntax of double programs. Only the remove benchmark requires partitioning for a successful analysis with the polyhedra domain. Four other benchmarks are analyzed very efficiently with the non relational interval domain, thanks to the p semantics. Partitioning improves the precision on three other, but reduces efficiency. Nonetheless, some benchmarks, such as LoopSub, cannot be analysed conclusively using a non relational numeric domain with semantics D p or p . Indeed, related patches exchange the roles of two variables a and b, so that the challenge is not to infer a

1 = a 2 ∧ b 1 = b 2 , but a 1 = b 2 ∧ b 1 = a 2 .
We therefore developed a dedicated abstract domain, to refine D p with automatically inferred variable equalities. This domain is based on union-find data structure that maintains a partitioning of the set V 1 ∪ V 2 ∪ Q of program variables. Two variables are part of the same equivalence class if they are guaranteed to be equal. The associate abstract lattice is the dual of the standard geometric lattice of partitions of a finite set: a b means that partition b refines partition a, i.e. every equivalence class of a is a union of classes of b;

is the set of singleton variables; and the smallest non ⊥ element is the whole set of variables. This abstract lattice has finite height, so we use union in place of widening. The LoopSub benchmark is analysed successfully using a reduced product between intervals and this domain.

D1 (polyhedra) D 1 (octagon)

Handling streams

All benchmarks of table 18 were analyzed using fixed-length queues of length 1, as the related works do not handle input streams. Note that abstracting infinite input streams with fixed-length queues of length 1 is also enough to analyze some patches of infinite-state programs with unbounded loops reading from a stream (e.g. a file), even when patches reorder input statements across the body of unbounded loops. Fig. 19 shows an example. This patch reorders input statements in the loop, and changes the number of input statements in terminating executions. The loop is unbounded, and the program is infinite-state. Terminating executions of the left and right projections compute equal values for s, though possibly not for x. This double program is analyzed successfully with D 1 , using any relational numerical domain: 33 ms for polyhedra, 43 ms for octagon, and 18 ms for the reduced product between the domains of intervals and variable equalities. To the best of our knowledge, no previous work has sound and precise automatic analyses for patches of this type.

In the bounded abstraction of streams, the unbounded FIFO queue represents the subsequence of input values read by the program ahead in the sequence, and not yet read by the program behind. Though we are bounding this queue in the abstract, we retain precise information on executions reading arbitrary long input sequences. The bounded queue allows retaining relational information between all input values read with delays less or equal to the bound, while non relational (interval) information is retained for values read with larger delays. Fig. 20 shows a simple example. Using a queue of length 1 is enough to infer the range of variable s in both projections of the double program. On the contrary,

Conclusion

We presented a static analysis for software patches. Our method is based on abstract interpretation, and parametric in the choice of an abstract domain. We presented a novel concrete collecting semantics, expressing the behaviors of two syntactically close versions of a program at the same time. This semantics deals with programs reading from unbounded input streams. We also introduced a novel numeric domain to bound differences between the values of the variables in the two programs, which has linear cost. We implemented a prototype and experimented on a few small examples from the literature.

In future work, we will consider extensions to larger, and non purely numeric programs, towards the analysis of realistic patches. We will also extend our method to characterize the semantic differences between two non equivalent versions of program. We will also investigate to what extend our approach could generalize to portability analysis, a dual problem where we wish to compare the semantics of the same program in two different environments. We plan to experiment with other abstract domains for our analysis, such as zonotopes. Finally, we will investigate the connections between our semantics and information flow problems. Indeed, as a side-effect of our method, our analysis is able to prove

+Fig. 1 .

 1 Fig. 1. Patch on remove.c of Coreutils (between v6.10 and v6.11)

1Fig. 2 .

 2 Fig. 2. Execution environments for cache fstatat

Fig. 5 .

 5 Fig. 5. Syntax of simple and double programs

  ). The semantics of a double statement s ∈ dstat, denoted D s ∈ R ω → P(D × D ), describes the relation between input and output states of s, which are pairs of states of simple programs, for a given shared sequence of input values. The definition for D s is shown on Fig. 6, in relational style. It is defined by induction on the syntax, so as to allow for modular, joint analyses of double programs that maintain input-output relations on the variables. Note that D is parametric in S. The semantics for the empty program is the diagonal, identity relation ∆ D . The semantics D s 1 s 2 for the composition of two syntactically different statements reverts to the pairing of the simple program semantics of individual simple statements s 1 and s 2 . Note that D s 1 s 2 σ = D s 1 skip σ D skip s 2 σ for any σ ∈ R ω , where we use the symbol to denote the left composition of

Fig. 6 .

 6 Fig. 6. Denotational concrete semantics of double programs

S

  V ← input(a, b) of simple input statements, input(a, b) returns only if the input value at the current index is in the range [a, b]. Therefore, it should be considered a semantic error if P 1 and P 2 use different ranges [a 1 , b 1 ] = [a 2 , b 2 ]

  problems. For instance, the D semantics distinguishes the two programs 21(a) and 21(b) shown on Fig 21, which will be presented in the conclusion.

  We then lift the semantics Ŝ1 s and Ŝ2 s to double programs. The definition of D s ∈ P( D × D) is very similar to that of D s . It can be obtained by removing σ parameters from Fig.6, except for the composition of syntactically different statements D s 1 s 2 and conditions F c 1 c 2 We thus only show the definitions of these relations on Fig.10. Following the particularization of simple statement semantics, the semantics for double statements and conditions compose the semantics of their left and right projections Dk s k and Fk c k , where Dk and Fk operate on simple statements and conditions only. Note that the order of the composition is arbitrary, and not significant, as D1 s D2 t = D2 t D1 s , and likewise for F1 c and F2 d . Finally, we formalize the relation between the abstract semantics D and the concrete collecting semantics D.

Proposition 2 .

 2 D is a sound and complete abstraction of D: D = α F (D).

Fig. 11 .

 11 Fig. 11. Abstraction of FIFO queues to fixed length p ≥ 1

11 . 3 .

 113 Queues from D are truncated whenever |δ| > p, and padded with zeros whenever |δ| < p. A formalization of this abstraction is shown on Fig. Proposition For all p ≥ 1, the pair (α p , γ p ) defined in Fig. 11 is a Galois embedding. Let p ≥ 1. Starting from semantics D, we now give a formal definition for the abstract double program semantics Dp resulting from this second abstraction step. Simple programs To this aim, we first define the semantics Ŝp k s ∈ P( Êp × Êp ) of simple programs, where Êp E × Z × R p , and k ∈ {1, 2}. Fig. 12 shows the semantics of Ŝp 1 V ← input(a, b) . Mutatis mutandis, the case of Ŝp 2 is similar. Intuitively, this semantics distinguishes between three cases: 1. If program P k is ahead of the other program in the input sequence, or at the same point, then a new successful input read operation produces a fresh Ŝp 1 s ∈ P( Êp × Êp) Ŝp 1 V ← input(a, b)

Proposition 4 .

 4 formalize the relation between the abstract semantics Dp and the previous abstraction D of the concrete collecting semantics. For all p ≥ 1, Dp is a sound and optimal abstraction of D: Dp = α p ( D).

Fig. 18 .

 18 Fig. 18. Benchmarks

Fig. 19 . 2 Fig. 20 .

 19220 Fig. 19. Reordering reads from an input stream

  12. Abstract semantics of simple program P1 with queues of length p ≥ 1. The case of P2 is similar. input value, and adds it on top of the queue, discarding the value at the bottom at the queue. 2. If program P k is behind the other program in the input sequence, and the delay is less than the size of the input queue, then a new successful input read operation retrieves the value in the queue indexed by this delay, and resets this value to zero. 3. If program P k is behind the other program in the input sequence, and the delay is more than the size of the input queue, then a new successful input read operation produces a fresh input value, and leaves the queue unchanged.

Coreutils

only 20 loop iterations

only 5 loop iterations

only 32 values of len

This work is performed as part of a collaborative partnership between Sorbonnne Université / CNRS (LIP6) and Airbus. This work is partially supported by the European Research Council under the Consolidator Grant Agreement 681393 -MOPSA.

David Delmas and Antoine Miné

This is required at least on BeOS and Haiku. master v8.31 … v6.

p c ← c + b = { (s1, (((a1, b1, c1 + b1, i1, r1), ((a1 + δa) -a1, (b1 + δb) -b1, ((c1 + δc) + (b1 + δb)) -(c1 + b1), (i1 + δi) -i1, (r1 + δr) -r1), δ, q)) | H1 } = { (s1, ((a1, b1, c1 + b1, i1, r1), (δa, δb, δc + δb, δi, δr), δ, q)) | H1 } p r ← c c + 1 = { (s1, ((a1, b1, c1, i1, c1), ((a1 + δa) -a1, (b1 + δb) -b1, ((c1 + δc) -c1, (i1 + δi) -i1, (c1 + δc + 1) -c1)), δ, q) | H1 } = { (s1, ((a1, b1, c1, i1, c1), (δa, δb, δc, δi, δc + 1), δ, q)) | H1 } where s1 ((a1, b1, c1, i1, r1), (δa, δb, δc, δi, δr), δ, q) and H1 s1 ∈ R 10 × Z × R p p skip s , for simple statement s. Nonetheless, we add some particular cases, to gain both efficiency and precision on δV , for all variables V , through simple symbolic simplifications. These particular cases are displayed on Fig. 17. Note that we use the syntactic renaming operator τ 2 , defined by induction on the syntax, to replace variables V 2 of the right projection of a double program by their abstraction V 1 + δV . The first particular case is that of input statements V ← input(a, b) for both programs, in environments such that both programs have read the same number of input values, i.e. δ = 0, where δ represents the difference between input indexes. In this case, we may assign δV ← 0 directly, and leave δ unchanged. that two sets of executions of the same program compute equal values for some outputs. This is useful for proving some information flow properties, such as secrecy. For instance, Fig. 21 shows two programs with public variable pub and secret variable sec. Our analysis is able to distinguish these two programs. Indeed, it compares the semantics of two versions of each program. In this case, both versions have exactly the same code, which is a form of self-composition [START_REF] Barthe | Secure information flow by self-composition[END_REF][START_REF] Müller | An analysis of universal information flow based on self-composition[END_REF].


Roda Bounaceur

Pierre-Alexandre Alexandre Glaude

Baptiste Sirjean

René Fournet

Pierre Montagne

Matthieu Vierling

Michel Moliere

Michel Molière

Prediction of Auto-Ignition Temperatures and Delays for Gas Turbine Applications

établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Among alternative fuels to natural gas, process gases, syngases and hydrogen-containing gases can find an increasing place as gas turbine fuels in the future. However most of them entail higher explosion risks than methane, namely in the event of a leak or during purges of pipes if air is used. More generally, many chemical processes use flammable gases and vapors under elevated pressures and high temperatures. The evaluation of auto-ignition hazards and safety concerns for a safe operation of such processes requires a sufficient knowledge of the lowest temperature at which spontaneous ignitions can take place. The Auto-Ignition Temperature data (AITs) found in the literature are usually determined by applying standardized test methods that are based on small vessels and are performed at atmospheric pressure. However, AITs are not fixed data but largely depend on the equivalence ratio, the pressure as well as the volume since convective transport can influence the tests. Therefore, the AIT values measured at atmospheric pressure and lab scale are often not applicable in industrial environments. The auto-ignition of a gas mixture is a complex phenomenon that is influenced by many factors, which can be classified into three categories: (i) "intrinsic parameters" that are linked to the gas mixture itself (nature and concentration of the reagents, pressure, presence of additives, nature of the oxidizer…) ; (ii) "extrinsic parameters" which are dependent on the test apparatus (volume of the vessel, nature of the wall, flow motion…), and (iii) parameters linked to the method of detection of the ignition (auto-ignition criterion). As a first observation, the auto-ignition temperature is strongly dependent on the nature of the fuel. As can be seen in Table 1, the AIT of hydrocarbon/air mixtures decreases with increasing molecular weight and chain length [START_REF] Chemsafe | Database of evaluated safety characteristics[END_REF]. The AIT is also higher for branched hydrocarbons than for linear hydrocarbons. Some attempts were done to correlate the AITs of pure hydrocarbons with the average carbon chain length [START_REF] Zabetakis | Flammability characteristics of combustible gases and vapours[END_REF]. [START_REF] Norman | Influence of process conditions on the auto-ignition temperature of gas mixtures[END_REF], ethane [6][12], propane [START_REF] Kong | Autoignition of CH4/air, C3H8/air, CH4/C3H8/air and CH4/CO2/air using a 1l ignition bomb[END_REF][13], n-butane [14][15], or blends that are representative of natural gas [START_REF] Kong | Autoignition of CH4/air, C3H8/air, CH4/C3H8/air and CH4/CO2/air using a 1l ignition bomb[END_REF] or LPG [START_REF] Norman | Influence of process conditions on the auto-ignition temperature of gas mixtures[END_REF]. Usually, the lowest auto-ignition temperature is not reached under the stoichiometric conditions, but for richer mixtures i.e. between the stoichiometric concentration and the upper flammability limit [START_REF] Bartknecht | Explosionsschutz, Grundlagen und Anwendung[END_REF]. Methane/air mixtures represent an exception to this rule: the lowest AIT of methane/air mixtures under 1 bar is reached in the lean range of 3.0-8.0 mole % of CH 4 (0.3 ≤ φ ≤ 0.8), while the stoichiometric concentration is to 9.5 mole % of CH 4 [START_REF] Kong | Autoignition of CH4/air, C3H8/air, CH4/C3H8/air and CH4/CO2/air using a 1l ignition bomb[END_REF]. In the same conditions, the minimum is reached at φ=4 (15 %mol.) for a propane/air mixture. An increase in pressure generally decreases the auto-ignition temperature of a gas mixture [START_REF] Steinle | High pressure combustion -Ignition temperatures to 1000 bar[END_REF]. Note worthily, while many processes in the chemical industry are conducted at elevated pressure, experimental data are mainly obtained under atmospheric conditions. It has been shown that a larger experimental vessel can lead to lower AITs [START_REF] Steinle | High pressure combustion -Ignition temperatures to 1000 bar[END_REF], because of a decrease of the ratio between the heat exchanged at the walls and the heat of reaction released in the volume. The nature of the walls is also of importance since the material can give rise to chemical reactions (creation or destruction of free radicals) or develop a physical effect (source or sink of heat, adsorption of intermediates etc.). Wall treatments of the vessel have shown a strong influence on the AITs [START_REF] Robinson | The auto-ignition temperature of methane[END_REF]. The most commonly used auto-ignition criterion is the visual observation of a flame but this method is applicable only to visible flames, require a test setup with a visual access and works in absence excessive soot. The visualization is more difficult at high pressure. Other methods rely on temperature or pressure recordings or the analysis of the reaction products that can replace the visual criterion, but the choice of the particular value of temperature or pressure rise may have a strong impact on the resulting AIT. For instance, a change of the temperature rise criterion from 50 K to 200 K can have a critical effect on the auto-ignition limit. The multiplicity of the factors influencing the AIT makes it difficult to elaborate a standardized determination method. A large number of standards actually exist e.g.: EN 14522 [START_REF]Determination of the minimum ignition temperature of gases and vapors[END_REF], DIN 51 794 [START_REF] Din | Bestimmung der zündtemperatur[END_REF], ASTM E 659-78 [START_REF]Standard test method for autoignition temperature of liquid chemicals[END_REF], ASTM D2155-66 [START_REF] Astm D | Standard test method of reaction threshold temperature of liquid and solid materials[END_REF]. ASTM D2883-95 applies to the auto-ignition temperature of liquids and solids at high pressure, but is unfortunately unsuitable for gases. Consequently many teams use the experimental setup that is the most adapted to their specific applications. As a matter of fact, the auto-ignition temperature of methane determined by different test methods over the last thirty years has known a variation between 813K and 923K [START_REF] Norman | Influence of process conditions on the auto-ignition temperature of gas mixtures[END_REF]. Besides hardware aspects, a number of experimental techniques exist for the generation of the auto ignition event, such as: closed vessels, rapid compression machines, shock tubes or continuous flow reactors. This wide panel of techniques is useful to cover the determination of auto-ignition delay times over large ranges of temperature, pressure and time scales.

Considering the complexity of this important topic, the team has decided to approach the auto-ignition properties at elevated pressures by means of comprehensive detailed kinetic models. The objective has been the assessment of the auto-ignition temperatures (AIT) and auto-ignition delay times of a wide range of fuels including hydrogen and covering namely natural gas, LPG and syngas. In overall, the gaseous species covered are the following ones: H 2 , CO, CH 4 , light alkanes up to C 5 and inert gases such as N2 and CO2. After assessing different kinetic models available in the literature against experimental data also taken from the literature, the auto-ignition properties of several fuels and air mixtures have been extensively evaluated in function of pressure and equivalence ratio using the best performing model.

KINETIC MODELING

Several comprehensive kinetic models for the oxidation and the combustion of light hydrocarbons have been proposed in the literature. However, most of these mechanisms have been designed for burner or engine conditions and are valid only for high temperature combustion (>1000 K), while kinetic data and mechanisms in the low temperature region are scarce. Flame conditions are far from auto ignition conditions in which the reactivity is very low and specific reactions that can be neglected at higher temperature may become critical paths.

Flames have typical timescales much shorter (e.g. milliseconds instead of minutes) than auto-ignition processes where the chemistry of the oxidation may be an intermediate between those involved in a flame and during the degradation in the atmosphere. The formation of peroxy free radicals through the oxidation by oxygen of alkyl radicals coming from the fuel represents critical steps since they yield hydroperoxides, which are the branching agents responsible for the auto acceleration of the reaction. The oxidation of hydrocarbons at low temperature follows a general scheme summarized by the following reactions:

In the case of light fuel species such as methane and ethane, important intermediates are methylperoxy CH3OO and ethylperoxy C 2 H 5 OO radicals, which react in bimolecular reactions to produce the branching agents CH 3 OOH and C2H5OOH. Many models miss some of these reactions that are negligible at higher temperature but are essential to correctly simulate AITs. Among the models available in the literature, a popular one is GRI-mech [START_REF] Smith | GRI-Mech 3.0[END_REF] that has been optimized for the combustion of methane at high temperature. Another comprehensive mechanism devoted to the combustion of methane has been proposed by the University of Leeds [START_REF] Hughes | Development and testing of a comprehensive chemical mechanism for the oxidation of methane[END_REF]. The combustion of natural gas, as a mixture of light hydrocarbons, is the subject of GDF-Kin [START_REF] Ferrières | Experimental and numerical investigation of low-pressure laminar premixed synthetic natural gas/O2/N2 and natural gas/H2/O2/N2 flames[END_REF] and Konnov's model [START_REF] Konnov | The pseudo-catalytic promotion of nitric oxide oxidation by ethane at low temperatures[END_REF], which have been regularly up-dated. Some models for the combustion of light alkanes up to n-butane have been developed in LLNL that includes low temperature chemistry [START_REF] Marinov | Aromatic and polycyclic aromatic hydrocarbon formation in a laminar premixed n-butane flame[END_REF] or have been validated over a wide range of pressure and equivalence ratio (NUIG [START_REF] Donato | Ignition and Oxidation of 50/50 Butane Isomer Blends[END_REF]). All these models have been validated against experimental ignition delay times, but at temperatures much higher than AIT.

A specific model, LRGP2014, has been created by our group based on own reaction bases and using the software EXGAS, which is an automatic mechanism generation tool [START_REF] Buda | Progress toward a unified detailed kinetic model for the autoignition of alkanes from C4 to C10 between 600 and 1200 K[END_REF]. This software developed in Nancy for several years allows the automatic generation of mechanisms for the gas-phase oxidation of hydrocarbons. It provides reaction mechanisms composed of three parts. A comprehensive primary mechanism contains only the reactions of the initial organic compounds, here propane, n-butane and n-pentane, and oxygen. The additions of alkyl radicals to oxygen molecules and the subsequent reactions leading to the formation of oxygenated compounds such as peroxides, aldehydes, ketones, and cyclic ethers, which are important below 1000 K, are considered to properly predict the low temperature chemistry. A comprehensive C 0 -C 2 reaction base includes all the reactions involving radicals or molecules containing less than three carbon atoms [START_REF] Glaude | Experimental and Modeling Study of Premixed Laminar Flames of Ethanol and Methane[END_REF]. Reactions of methane, ethane, hydrogen and CO are included in this base. A lumped secondary mechanism contains the reactions consuming the molecular products of the primary mechanism (e.g ketohydroperoxides, alkenes, cyclic ethers, aldehydes, ketones), which do not react in the reaction base. Thermochemical data for molecules or radicals are automatically calculated based on group additivity methods. Kinetic data are estimated either based on thermochemical kinetics methods, or on quantitative structurereactivity relationships obtained from literature reviews. This system has been used to generate validated mechanisms for the low temperature oxidation of n-butane, isomers of pentane, nheptane and iso-octane and large alkanes [START_REF] Buda | Progress toward a unified detailed kinetic model for the autoignition of alkanes from C4 to C10 between 600 and 1200 K[END_REF][29] [START_REF] Biet | Experimental and Modeling Study of the Low-Temperature Oxidation of Large Alkanes[END_REF]. An extension of this system has also been achieved to model the oxidation of ethers and methyl esters using a comprehensive low temperature mechanism [START_REF] Glaude | Modeling of the oxidation of methyl esters-Validation for methyl hexanoate, methyl heptanoate, and methyl decanoate in a jet-stirred reactor[END_REF]. The final mechanism contains 209 species that are involved in 1473 reactions. The LRGP2014 model can be obtained upon request.

In the present work, the performances of these mechanisms were checked against some typical experimental results from the literature. Simulations were performed using the CHEMKIN II software [32] developed for the resolution of the mass and energy equations relevant to main laboratory reactors. In particular SENKIN, which is dedicated to the simulation of internal combustion engines, was used for the calculation of ignition delay times and the determination of AITs. AITs have been calculated by mimicking the Standard ASTM E 659-78 which considers that there is auto-ignition if a flame can be observed before a delay of 10 minutes after the load of the reagents in a 500 cm 3 silica glass cylinder. In the calculations, auto-ignition was assumed to have occurred when a 400K increase of the temperature was reached. Calculations assume a constant volume and a typical heat loss rate through glass walls (h = 19 W m 2 K -1 ) [START_REF] Pekalski | Theoretical and experimental study of explosion safety of hydrocarbons oxidation at elevated conditions[END_REF]. It is important to stress the fact that this simple 0D simulation method does not capture the great complexity of the heat and convective mass transfer processes inside the test cylinder during real auto-ignition experiments.

VALIDATION OF THE MODEL

AITs of methane, ethane, and propane/air mixtures in function of the equivalent ratio were calculated at 1 bar using the seven different models that have been presented above and are reviewed below. The experimental decrease of the minimum AIT with the increasing chain length in hydrocarbons, shown in Table 1, is not reproduced by three of these models (GRImech [START_REF] Smith | GRI-Mech 3.0[END_REF], Leeds [START_REF] Hughes | Development and testing of a comprehensive chemical mechanism for the oxidation of methane[END_REF], and NUIG [START_REF] Donato | Ignition and Oxidation of 50/50 Butane Isomer Blends[END_REF]) which predict higher AIT for ethane than for methane. Indeed, these models were developed for conditions much different from those that prevail in AIT. In fact they do not contain any reactions involving ethylperoxy and propylperoxy radicals needed to reproduce the low temperature reactivity of the parent fuels. As far as the others models are concerned, they account for the difference of reactivity between C1, C2 and C3 species even though large discrepancies exist between the different mechanisms. Once again, the lack of low temperature reactions in some of these models can explain these differences. The variation of AIT in function of pressure and equivalence ratio for different fuel/air mixtures was also investigated. An inversion between the AITs of methane and ethane calculated with the model of Konnov [START_REF] Konnov | The pseudo-catalytic promotion of nitric oxide oxidation by ethane at low temperatures[END_REF] was observed. This latter was then discarded in the next phase of the study.

With the three remaining models, minimum AITs at 1 bar were calculated for equivalent ratio ranging from 0.1 to 15 and compared with the CHEMSAFE data [START_REF] Chemsafe | Database of evaluated safety characteristics[END_REF]. Figure 1 shows this comparison. The LLNL model [START_REF] Marinov | Aromatic and polycyclic aromatic hydrocarbon formation in a laminar premixed n-butane flame[END_REF] leads to AIT of n-butane higher than that of propane, in contradiction with the real trend.

GdF-Kin [START_REF] Ferrières | Experimental and numerical investigation of low-pressure laminar premixed synthetic natural gas/O2/N2 and natural gas/H2/O2/N2 flames[END_REF] yields an AIT of n-pentane equivalent to that of n-butane. In fact, both of these models have been validated at low temperature for compounds up to C 3 but none of them contains a complete low temperature mechanism for C 4 and C 5 species. In conclusion, it appears that, among all the compared models, only the LRGP2014 model proves robust enough to correctly reproduce the AIT dependence on the various operating conditions. Therefore, in the next phase of the study, which is set out below, this model was further tested against extensive literature data. Steinle and Franck [START_REF] Steinle | High pressure combustion -Ignition temperatures to 1000 bar[END_REF] studied the oxidation of methane/air mixtures at very high pressure in cylindrical and spherical vessels. The comparison between simulated results and experimental data is visible in Figure 2a, showing a correct agreement. Caron et al. [START_REF] Caron | Pressure dependence of the auto-ignition temperature of methane/air mixtures[END_REF] and Norman [START_REF] Norman | Influence of process conditions on the auto-ignition temperature of gas mixtures[END_REF] investigated several methane/air mixtures at different pressures and concentrations in a spherical vessel. Figure 2b shows the pressure/temperature region obtained for a mole fraction of methane equaling 60 % in air, corresponding to an equivalence ratio of 14.29. A fair agreement between experimental data and simulations is obtained, especially keeping in mind that the experimental uncertainties in AIT measurements are tens of Kelvins, as discussed above. Experimental AITs of ethane, propane, n-butane and n-pentane have also been simulated with the LRGP2014 model. Figure 3 illustrates the evolution of AITs of propane and n-butane as a function of pressure. The model reproduces fairly well the trend of the AITs of propane (Figure 3a) measured in a 1 liter ignition vessel up to 20 bar [START_REF] Kong | Autoignition of CH4/air, C3H8/air, CH4/C3H8/air and CH4/CO2/air using a 1l ignition bomb[END_REF]. The AITs of n-butane/air mixtures measured in a 8L spherical bomb [START_REF] Van Den Schoor | Influence of the ignition source location on the determination of the explosion pressure at elevated initial pressures[END_REF] are also well reproduced up to 25 bar (Figure 3b). In that case, it appears that AITs are not very sensitive to the pressure. The behavior of gas mixtures is of most interest in real applications. Kong et al. [START_REF] Kong | Autoignition of CH4/air, C3H8/air, CH4/C3H8/air and CH4/CO2/air using a 1l ignition bomb[END_REF] have studied the auto-ignition of methane/propane/air mixtures in a 1 liter ignition bomb. Figure 4 compares experiments and simulations for different equivalence ratios. Both trends and orders of magnitude are rather well respected by the LRGP2014 model, even if the calculations give lower AITs for rich mixtures. A further validation of the LRGP2014 model was performed against ignition delay times (AID). Auto-ignition delay times of methane/hydrogen mixture with a hydrogen mole fraction ranging from 0 to 100%, were experimentally measured in a shock tube by Zhang et al. [START_REF] Zhangy | Experimental and modeling study on auto-ignition characteristics of methane/hydrogen blends under engine relevant pressure[END_REF]. Pressure was kept at 18 bar and temperatures behind the reflected shock waves were in the range of 900 to 1750 K (Figure 5). Both the AID values and the trends obtained with LRGP2014 are in a good agreement with the experimental data irrespective to the fuel composition, even though the reactivity is a slightly overestimated for the lower hydrogen fractions. Some validations were also performed with pure light alkanes. Figure 6 displays some comparisons between simulations and experimental auto-ignition delay times obtained in shock tubes for methane, ethane and n-butane. Figure 6a relates to stoichiometric mixtures of methane/oxygen/argon at 3 and 10 bar [START_REF] Lifshitz | Shock-tube investigation of ignition in methane-oxygenargon mixtures Combust[END_REF]. Figure 6b summarizes the influence of both the equivalence ratio and the concentration of ethane under moderate pressure [START_REF] Hidaka | Shock-Tube and modelling study of ethane pyrolysis and oxidation[END_REF]. Figure 6c refers to the AID of n-butane at different pressures [START_REF] Horning | A study of the high-temperature autoignition and thermal decomposition of hydrocarbons[END_REF]. For the three fuels, the LRGP2014 model simulates fairly well the ignition-delays and the temperature dependence. Ethane and propane are two major non-methane alkanes components of natural gas. The combustion of natural gas can be represented as that of a mixture of methane with light alkanes. Figure 7 presents the comparison between simulated results and experiments of such mixtures. Figure 7a displays the AIDs of a methane/ethane mixture, for temperature ranging between 800 and 1200 K, with a pressure of about 20 atm and an equivalence ratio around 0.5 [START_REF] Vries | Autoignition of methane-based fuel blends under gas turbine condiotions[END_REF]. Lamoureux and Paillard [START_REF] Lamoureux | Natural gas ignition delay times behind reflected shock waves: Application to modelling and safety[END_REF] studied a natural gas/oxygen/argon mixture in a shock tube: figure 7b shows the experimental data they found for an Algerian natural gas modeled as the following blend: 89.6%CH4 + 8.4%C2H6 + 1.2%C3H8 + 0.4%C4H10 + 0.4%N2 ; the equivalence ratio equaled 0.5 and the pressure was 6 bar.

Here again, the LRGP2014 model successfully reproduces the sets of experiments as shown in figures 7a and 7b. To summarize, multiple comparisons between experimental data and LRGP2014 simulations were performed, involving a large number of mixtures, equivalence ratio, pressures, temperatures and test setups. The values and the trends agree fairly well, considering the considerable experimental uncertainties in the measurement of AITs. The maximum gap between the experimental and calculated AIT data does not exceed, in most cases, 50 K which allows considering that the LRGP2014 model is appropriate for the prediction of AITs.

USE OF THE MODEL FOR PREDICTIVE CALCULATIONS

For safety purpose, the model has been used to predict the minimum AIT of several paradigmatic gas fuels in function of pressure and equivalence ratio. The compositions of the selected gas mixtures are shown in Table 2. Mixture B1 is methane taken as a reference. Mixture B2 represents a gas that is very rich in alkanes. Mixture B3 stands for methane enriched in hydrogen and mixture B4 represents a real natural gas typically burned in gas turbines. Mixture B5 stands for a Coke Oven Gas and mixture B6 is for a low BTU Blast Furnace Gas. In all cases, the equivalence ratio was varied from 0.2 to 4.0 and the pressure from 1 to 25 bar. In all simulations, a closed vessel with a volume of 200 cm 3 was considered, with a heat transfer coefficient of 19 W.m -2 .K -1 at the wall and a time of 5 min for the appearance of auto-ignition. Figure 8 illustrates the results obtained with the syngas B5; they can be used in engineering studies. While the detailed kinetic model enables the calculation of the AIT of individual mixtures in given conditions, it was deemed interesting to develop an analytical, multi-parameter correlation of AIT as calculated with LRGP2014, knowing that such fitting will be a pure mathematical expression without any physical meaning. To that end, a data fit by means of a mathematical expression has been performed for all mixtures.

In order to derive a global expression, the different parameters were reproduced step by step. First, the variation of the AIT as a function of the equivalence ratio was represented by means of the following function: = + (1) The value of the power coefficient α2 was kept constant and equal to -0.6. Seven different expressions of α 0 and α 1 , corresponding to the seven calculation pressures, were then obtained (Table 3). The second and the third steps consisted in fitting the coefficients αi as a function of pressure and gave an analytical expression of α 0 (equation 2) and α 1 (equation 3):

= + (2) = + - (3)
where P is the pressure in bar, and k i parameters determined for each reacting blend. A power expression was found suitable to correlate the first parameter α 0 , while it was necessary to use a more complex log-normal expression to correctly fit the coefficient α1 over the entire range of conditions. Figure 9 illustrates the correlation of the values in Table 3 by these two latter expressions. Eventually, one obtains a fully analytical representation, named "the BGSF correlation", which represent the variation of the AIT as a function of the equivalence ratio and the pressure, with the AIT in Kelvin and the pressure in bar:

= + + + - . (4)
Table 4 summarizes the coefficients for the blends studied. This expressions are valid for pressures from 1atm up to 25 atm, and equivalence ratios ranging from 0.4 to 4. In the case of the gas B1 (100% methane) a special behavior was obtained at 1 bar. Indeed, as experimentally observed at atmospheric pressure [START_REF] Kong | Autoignition of CH4/air, C3H8/air, CH4/C3H8/air and CH4/CO2/air using a 1l ignition bomb[END_REF], the AIT of methane reaches a minimum for an equivalence ratio close to the stoichiometry, i.e. much lower than for other alkanes. For richer mixtures, the AIT of methane increases. Therefore the expressions of the k i coefficients contained in -.

CONCLUSION

The aim of this study was to numerically investigate the influence of process conditions on the auto-ignition temperature of different fuel/air mixtures. Although many AITs of hydrocarbon-air mixtures can be found in the literature, these values are generally determined at atmospheric pressure according to various standard test methods. Since many industrial processes operate at higher pressures, an accurate knowledge of the auto-ignition temperatures in these conditions is essential for the safe and rational operation of those processes. After a description of the key factors influencing the auto-ignition temperature, several chemical models, available in the literature, have been tested in order to find the most robust one. The low temperature and the long time scale involved in spontaneous auto-ignition events require the inclusion in the kinetic models of specific reaction channels that are negligible in usual flame conditions. A number of models that are recognized as robust in usual flame conditions, proved unreliable when extrapolated in the AIT conditions that are of interest in the present study. This robustness test led to retain the LRGP2014 model that has been developed by the LRGP laboratory, since it yielded fairly good fits through a large number of cross checks between experiments and simulations. The specific objective of this study was the prediction of the auto-ignition temperature of fuel/air mixtures depending on the pressure and the equivalence ratio. All the results have been successfully fitted by means of a BGSF correlation which enables a direct, simple analytical evaluation of the AIT for mixtures of interest in the industry, namely in gas turbine applications.

DISCLAIMER

The information contained in this technical paper represents the best and most current information owned by the authors on the subject and is believed to be correct. However the authors and their respective organizations make no representations or warranties regarding the accuracy and will not be responsible for damages resulting from use or reliance upon this information.

Figure 1 :

 1 Figure 1: Minimum auto-ignition temperature vs. number of carbon atoms for different fuel/air mixtures at 1 bar.

Figure 2 :

 2 Figure 2: AIT of methane/air mixture as a function of pressure (a) equivalence ratio 2, (b) equivalence ratio 14.3. Points are experimental data, lines simulations.

Figure 3 :

 3 Figure 3: AIT of (a) propane/air and (b) n-butane/air mixture as a function of pressure. Points are experimental data, lines simulations.

Figure 4 :

 4 Figure 4: AIT of methane/propane/air mixtures at P=1bar and different equivalence ratios. Points are experimental data, lines simulations.

Figure 5 :

 5 Figure 5: Auto-ignition delay times for methane/hydrogen/ oxygen/argon mixtures. Points are experimental data, lines simulations.

Figure 6 :

 6 Figure 6: Auto-ignition delay times for methane (a), ethane (b), and n-butane (c) in shock tube. Points are experimental data, lines simulations.

Figure 7 :

 7 Figure 7: Auto-ignition delay times for (a), methane/ethane (b) natural gas in shock tube. Lines are simulations.

Figure 8 :

 8 Figure 8: Simulated AITs for the blend B5 as a function of pressure and equivalence ratio.

Figure 9 :

 9 Figure 9: Fit of coefficients of the AIT vs. φ law as a function of pressure in the case of mixture B5.

Table 1 .

 1 Minimum auto-ignition temperature (AIT) of fuels at standard temperature and pressure in the literature (K)

	Fuel		Reference publication
		[1]	[2]	[3]	[4]
	Hydrogen	810	845	845	833
	Methane	868	810	905	858
	Ethane	788	745	745	788
	Propane	743	739	766	743
	i-Butane	733	-	-	733
	n-Butane	638	688	678	703
	n-Pentane	533	557	505	-
	n-Hexane	503	-	-	-

Many experimental data have been recorded for individual fuel species, such as hydrogen

[START_REF] Beerer | Autoignition of Hydrogen and Air Inside a Continuous Flow Reactor With Application to Lean Premixed Combustion[END_REF]

, methane

[START_REF] Steinle | High pressure combustion -Ignition temperatures to 1000 bar[END_REF]

[7][8][9]

[START_REF] Caron | Pressure dependence of the auto-ignition temperature of methane/air mixtures[END_REF]

Table 2 .

 2 Composition of the studied fuels (%mol.)

Table 3 .

 3 Coefficients of the [AIT vs. φ] function for gas B5.

	P [bar]	1	5	9	13	17	21	25
	α0	811.8 708.1 689.6 682.4 678.9 675.9 673.7
	α1	16.38 41.66 35.67 30.30 25.99 23.68 21.52
	α2	-0.6	-0.6	-0.6	-0.6	-0.6	-0.6	-0.6

  Table 4 for BN1 are valid only for pressures higher than 2 bar. Values of AIT for methane/air mixture at 1 bar have been fitted with a simple polynomial expression as follows:

	, = + .	. -	.	+	.	-	.

Table 4 .

 4 Coefficients in equation (4) for the calculation of AITs of gas mixtures,1≤P≤25 bar, 0.4≤φ≤4. a

		B1 b	B2	B3	B4
	k0	668.8	-1539.8	641.0	584.2
	k1	212.5	2320.3	184.8	221.6
	k2	-0.77	-0.04	-0.46	-0.50
	k3	24.02	67.06	-8.13	35.36
	k4	36.51	45.20	61.49	36.04
	k5	4.90	15.56	5.39	4.44
	k6	1.35	0.90	2.28	1.56

a : coefficients related to fuel B5 and B6 can be provided based upon request b : only for P>1 bar.