Software for commercial aircraft is subject to the stringent certification processes described in the DO-178B standard, "Software Considerations in Airborne Systems and Equipment Certification." Issued in 1992, this document focuses strongly on the verification process, with a major emphasis on testing. In 2005, the avionics industry initiated an effort to update DO-178B, in large part to accommodate development practices (including formal verification techniques) that had matured since its publication. A revised standard, DO-178C, was issued in late 2011, incorporating new guidance that allows formal verification to replace certain forms of testing. In this article, the authors describe some of the new objectives and activities in the area of formal methods, explain how these methods may be used instead of testing in a DO-178C context, and summarize the practical experience of Dassault-Aviation and Airbus in successfully applying the new DO-178C approach. The first Web extra at http://youtu.be/tRtK4xOK-8o is part 1 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C. The second Web extra at http://youtu.be/BVI5J1GAQ30 is part 2 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C. The third Web extra at http://youtu.be/U3G1ZOoqg78 is part 3 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C. The fourth Web extra at http://youtu.be/WtlqS-JOHrA is part 4 of a video talk by Hervé Delseny, describing Airbus's use of formal methods to verify avionics software and summarizing the integration of formal methods in the upcoming ED-12/DO-178 issue C.

Deduction-based software verification tools have reached a maturity allowing them to be used in industrial context where a very high level of assurance is required. This raises the question of the level of confidence we can grant to the tools themselves. We present a certified implementation of a verification condition generator. An originality is its genericity with respect to the logical context, which allows us to produce proof obligations for a large class of theorem provers.

Frama-C is a source code analysis platform that aims at con- ducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive veri- fication, and testing, for safety- and security-critical software. Collabora- tive verification across cooperating plug-ins is enabled by their integra- tion on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.

Static analyzers should be correct. We used the random C-program generator Csmith, initially intended to test C compilers, to test parts of the Frama-C static analysis platform. Although Frama-C was already relatively mature at that point, fifty bugs were found and fixed during the process, in the front-end (AST elaboration and type-checking) and in the value analysis, constant propagation and slicing plug-ins. Several bugs were also found in Csmith, even though it had been extensively tested and had been used to find numerous bugs in compilers.

We present functional dependencies , a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.

We introduce parameterized rewrite systems for describing infinite families of finite string rewrite systems depending upon non-negative integer parameters, as well as ways to reason uniformly over these families. Unlike previous work, the vocabulary on which a rewrite system in the family is built depends itself on the integer parameters. Rewriting makes use of a toolkit for parameterized words which allows to describe a rewrite step made independently by all systems in an infinite family by a single, effective parameterized rewrite step. The main result is a confluence test for all systems in a family at once, based on a critical pair lemma classically based on computing finitely many overlaps between lefthand sides of parameterized rules and then checking for their joinability (which decidability is not garanteed).

We demonstrate the value analysis of Frama-C. Frama-C is an Open Source static analysis framework for the C language. In Frama-C, each static analysis technique, approach or idea can be implemented as a new plug-in, with the opportunity to obtain information from other plug-ins, and to leave the verification of difficult properties to yet other plug-ins. The new analysis may in turn provide access to the data it has computed. The value analysis of Frama-C is a plug-in based on abstract interpretation. It computes and stores supersets of possible values for all the variables at each statement of the analyzed program. It handles pointers, arrays, structs, and heterogeneous pointer casts. Besides producing supersets of possible values for the variables at each point of the execution, the value analysis produces run-time-error alarms. An alarm is emitted for each operation in the analyzed program where the value analysis cannot guarantee that there will not be a run-time error.

This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources...) but could have prevented the use of OCaml for this project if they had been missing.

ion The term \lambda τ1 x1, . . . , τn xn ; t denotes the n-ary logic function which maps x1, . . . , xn to t. It has the same precedence as \forall and \exists In this latter case, note that the two ’>’ must be separated by a space, to avoid confusion with the shift operator. ANSI/ISO C Specification Language CAT RNTL project 2.6 Logic specifications 39 term ::= \lambda binders ; term abstraction | extended-quantifier ( term , term , term ) extended-quantifier ::= \max | \min | \sum | \product | \numof Figure 2.12: Grammar for higher-order constructs Extended quantifiers Terms \quant(t1, t2, t3) where quant is max min sum product or numof are extended quantifications. t1 and t2 must have type integer, and t3 must be a unary function with an integer argument, and a numeric value (integer or real) except for \numof for which it should have a boolean value. Their meanings are given as follows: \max(i, j, f) = max{f(i), f(i+ 1), . . . , f(j)} \min(i, j, f) = min{f(i), f(i+ 1), . . . , f(j)} \sum(i, j, f) = f(i) + f(i+ 1) + · · ·+ f(j) \product(i, j, f) = f(i)× f(i+ 1)× · · · × f(j) \numof(i, j, f) = #{k | i ≤ k ≤ j && f(k)} = \sum(i, j,\lambda integer k; f(k)?1 : 0) If i > j then \sum and \numof above are 0, \product is 1, and \max and \min are unspecified (see Section 2.2.2). Example 2.28 Function that sums the element of an array of doubles. /*@ requires n ≥ 0 ∧ \valid(t+(0..n−1)) ; @ ensures \result ≡ \sum(0,n−1,\lambda int k; t[k]); @*/ double array_sum(double t[],int n) { int i; double s = 0.0; /*@ loop invariant 0 ≤ i ≤ n; @ loop invariant s ≡ \sum(0,i−1,\lambda int k; t[k]); @ loop variant n−i; */ for(i=0; i = Nil | Cons(A,list ); ANSI/ISO C Specification Language CAT RNTL project 40 Specification language logic-type-decl ::= type logic-type = logic-type-def ; logic-type-def ::= record-type | sum-type | type-expr type abbreviation record-type ::= { type-expr id (; type-expr id)∗ ;? } sum-type ::= | constructor (| constructor)∗ constructor ::= id constant constructor | id ( type-expr (, type-expr)∗ ) non-constant constructor type-expr ::= ( type-expr (, type-expr)+ ) product type term ::= term . id record field access | \match term { match-cases } pattern-matching | ( term (, term)+ ) tuples | { (. id = term ;)+ } records | \let ( id (, id)+ ) = term ; term match-cases ::= match-case match-case ::= case pat : term pat ::= id constant constructor | id ( pat (, pat)∗ ) non-constant constructor | pat | pat or pattern | _ any pattern | cst numeric constant | { (. id = pat)∗ } record pattern | ( pat (, pat)∗ ) tuple pattern | pat as id pattern binding Figure 2.13: Grammar for concrete logic types and pattern-matching introduces a concrete definition of finite lists. The logic definition /*@ logic integer list_length (list l) = @ \match l { @ case Nil : 0 @ case Cons(h,t) : 1+list_length(t) @ }; @*/ defines the length of a list by recursion and pattern-matching. 2.6.5 Hybrid functions and predicates Logic functions and predicates may take both (pure) C types and logic types arguments. Such an hybrid predicate (or function) can either be defined with the same syntax as before, or simply declared, but in the latter case the declaration should usually be augmented with a reads clause, with the syntax given in Figure 2.14, which extends the one of Figure 2.11. This feature is useful when a function or a predicate is not easily definable, but can be more easily axiomatized. ANSI/ISO C Specification Language CAT RNTL project 2.6 Logic specifications 41 logic-function-decl ::= logic type-expr poly-id parameters reads-clause ; logic-predicate-decl ::= predicate poly-id parameters? reads-clause ; reads-clause ::= reads locations logic-function-def ::= logic type-expr poly-id parameters reads-clause = term ; logic-predicate-def ::= predicate poly-id parameters? reads-clause = pred ; poly-id ::= id normal identifier | id type-var-binders identifier for polymorphic object | id label-binders normal identifier with labels | id label-binders type-var-binders polymorphic identifier with labels label-binders ::= { id (, id)∗ } Figure 2.14: Grammar for logic declarations with reads clauses Be it defined either directly by an expression or through a set of axioms, an hybrid function (or predicate) usually depends on one or more program points, because it depends upon memory states, via expressions such as: • pointer dereferencing: *p, p->f; • array access: t[i]; • address-of operator: x • built-in predicate depending on memory: \valid To make such a definition safe, it is mandatory to add after the declared identifier a set of labels, between curly braces. Expressions as above must then be enclosed into the \at construct to refer to a given label. However, to ease reading of such logic expressions, it is allowed to omit a label whenever there is only one label in the context. Example 2.30 The following annotations declare a function which returns the number of occurrences of a given double in an array of doubles between the given indexes, together with the related axioms. It should be noted that without the reads clauses, this axiomatization would be inconsistent, since the function would not depend on the values stored in t, hence the two last axioms would say both that a = b+ 1 and a = b for some a and b. /* nb_occ(t,i,j,e) gives the number of occurrences of e in t[i..j] * (in a given memory state labelled L) */ /*@ logic integer nb_occ{L}(double t[], integer i, integer j, @ double e) ANSI/ISO C Specification Language CAT RNTL project 42 Specification language @ reads t[..]; @*/ /* Notice that without label {L}, t[..] would be rejected. * With {L}, it is indeed a shortcut for \at (t[..],L). */ /*@ axiom nb_occ_empty{L} : @ ∀ double t[], integer i, integer j, double e; @ i > j =⇒ nb_occ(t,i,j,e) ≡ 0; @*/ // without {L}, term nb_occ(t,i,j,e) would be rejected /*@ axiom nb_occ_true{L} : @ ∀ double t[], integer i, integer j, double e; @ i ≤ j ∧ t[i] ≡ e =⇒ @ nb_occ(t,i,j,e) ≡ nb_occ(t,i,j−1,e) + 1; @*/ // without {L}, term ti would be rejected, here it is \at (ti,L) /*@ axiom nb_occ_false{L} : @ ∀ double t[], integer i, integer j, double e; @ i ≤ j ∧ t[i] 6≡ e =⇒ @ nb_occ(t,i,j,e) ≡ nb_occ(t,i,j−1,e); @*/ Example 2.31 This second example defines a predicate which indicates whether two arrays of the same size are a permutation of each other. It illustrates the use of more than a single label. Thus, the \at operator is mandatory here. Indeed the two arrays may come from two distinct memory states. Typically, one of the post condition of a sorting function would be permut{Pre,Here}(t,t). /* permut{L1,L2}(t1,t2,n) is true whenever t1[0..n−1] in state L1 * is a permutation of t2[0..n−1] in state L2 */ /*@ predicate permut{L1,L2}(double t1[], double t2[], integer n) @ reads \at(t1[..],L1), \at(t2[..],L2); @*/ /*@ axiom permut_refl{L} : @ ∀ double t[], integer n; permut{L,L}(t,t,n); @*/ /*@ axiom permut_sym{L1,L2} : @ ∀ double t1[], double t2[], integer n; @ permut{L1,L2}(t1,t2,n) =⇒ permut{L2,L1}(t2,t1,n) ; @*/ ANSI/ISO C Specification Language CAT RNTL project 2.6 Logic specifications 43 /*@ axiom permut_trans{L1,L2,L3} : @ ∀ double t1[], double t2[], double t3[], integer n; @ permut{L1,L2}(t1,t2,n) ∧ permut{L2,L3}(t2,t3,n) @ =⇒ permut{L1,L3}(t1,t3,n) ; @*/ /*@ axiom permut_exchange{L1,L2} : @ ∀ double t1[], double t2[], integer i, integer j, integer n; @ \at(t1[i],L1) ≡ \at(t2[j],L2) ∧ @ \at(t1[j],L1) ≡ \at(t2[i],L2) ∧ @ (∀ integer k; 0 ≤ k = Nil | Cons(A , list ); @ @ logic integer length (list l) = @ \match l { @ case Nil : 0 @ case Cons(h,t) : 1+length(t) } ; @ @ logic A fold_right ((A −> B −> B) f, list l, B acc) = @ \match l { @ case Nil : acc @ case Cons(h,t) : f(h,fold(f,t,acc)) } ; @ @ logic list filter ((A −> boolean) f, list l) = @ fold_right((\lambda A x, list acc; @ f(x) ? Cons(x,acc) : acc), Nil) ; @ @ } @*/ Module components are then accessible using a qualified notation like List::length . Predefined algebraic specifications can be provided as libraries (see section 3), and imported using a construct like

Bugs in programs implementing security features can be catastrophic: for example they may be exploited by malign users to gain access to sensitive data. These exploits break the confidentiality of information. All security analyses assume that softwares implementing security features correctly implement the security policy, i.e.are security bug-free. This assumption is almost always wrong and IT security administrators consider that any software that has no security patches on a regular basis should be replaced as soon as possible. As programs implementing security features are usually large, manual auditing is very error prone and testing techniques are very expensive. This article proposes to reduce the code that has to be audited by applying a program reduction technique called slicing. Slicing transforms a source code into an equivalent one according to a set of criteria. We show that existing slicing criteria do notpreserve the confidentiality of information. We introduce a new automatic and correct source-to-source method properly preserving the confidentiality of information i.e.confidentiality is guaranteed to be exactly the same in the original program and in the sliced program.

A termination proof search in CiME begins with computation of termination con- straints. These may be checked by ACRPO (5) or translated into Diophantine con- straints in order to obtain polynomial interpretations. In that last case, the finite domain constraint solver of CiME tries to find a solution. Our policy is to provide a tool for proving termination of the TRS one meets in practice. Hence, we focus on modu- lar/incremental proofs, a case for which the search for termination preserved under non-deterministic collapse is a particularly important issue. Basic Features. Several criteria may be used in CiME: The standard one (all rules strictly decrease) but also dependency pairs criteria (1), with or without marking of symbols, and with or without dependency graphs. Our extensions of dependency pairs to the AC case are also implemented (3). We use two kinds of cycle analysis for the dependency graph refinement: one which treats all strongly connected components (and which is, thus, very efficient) and one which treats all strongly connected parts of the graph; the latter being more powerful but of higher complexity than the former. The search for polynomial interpretations may be parameterized by the kind of polynomial to restrict to (linear, simple ou simple-mixed) and by the bound of their coefficients. In any case, AC-compatible interpretations will be used for AC-symbols. Restricting to linear polynomials leads to fewer and easier (smaller) constraints than restricting to more complex polynomials, but at the cost of some termination power. Similarly, restricting to very small coefficients leads to faster constraint solving but might be not enough to find a suitable ordering. Thus, in order to deal with TRS with numerous rules that are common in practice, and so as to make constraints as weak as possible, CiME makes use of powerful modular and incremental criteria.

This paper presents a general method for studying some quotients of the special linear group SL2 over the integers, which are of fundamental interest in the field of statistical physics. Our method automatically helps in validating some conjectures due to physicists, such as conjectures stating that a set of equations completely describes a finite given quotient of SL2. In a first step, we show that in the cases we are interested in, the usual presentation of finitely generated groups with some constant generators and a binary concatenation can be turned into an equivalent one with unary generators. In a second step, when the completion of the transformed set of equations terminates, we show how to compute directly the associated normal forms automaton. According to the presence of loops, we are able to decide the finiteness of the quotient, and to compute its cardinality. When the quotient is infinite, the automaton gives some hints on what kind of equations are needed in order to insure the finiteness of the quotient.