ABSTRACT. The safety and correctness of avionics software products is paramount, especially for safety-critical software. It is thus developed against stringent international regulations (DO-178). Nonetheless, the size and complexity of avionics software products have grown exponentially in the four last decades. Legacy methods, based on informal designs, testing and intellectual analysis, have been shown to scale poorly, as opposed to some formal techniques. Airbus have therefore been transforming the development processes of avionics software, taking advantage from sound formal methods to preserve safety, while improving cost-efficiency. The talk will report on this transformation.

ABSTRACT. Affine arithmetic is a well known tool to derive first order guaranteed approximations of general formulas over real numbers. It is also a useful tool in static analysis to keep track of linear correlations between program variables. However non-linear operations, like multiplications or divisions, introduce compensation terms to over-approximate the residue of the linearization process. Tight estimations of those terms are of utmost importance to obtain precise abstractions and thus a useful analysis. In this paper, we propose a new and simple technique to compute precise compensation terms for divisions.

ABSTRACT. Dynamic languages, such as JavaScript, PHP, Python or Ruby, provide a memory model for objects data structures allowing programmers to dynamically create, manipulate, and delete objects’ properties. Moreover, in dynamic languages it is possible to access and update properties by using strings: this represents a hard challenge for static analysis. In this paper, we exploit the finite state automata abstract domain, approximating strings, in order to define a novel abstract domain for objects. We design an abstract interpreter useful to analyze objects in a toy language, inspired by real-word dynamic programming languages. We then show, by means of minimal yet expressive examples, the precision of the proposed abstract domain.

ABSTRACT. The first objective of parallelization is to speed up the program execution. Typically, a program is split into multiple parts that are computed on different computation cores. A usual approach is to balance the load of each core, splitting the computation evenly among them. However, when the program performs computations in floating-point arithmetic, we should pay extra attention to their numerical accuracy. Indeed, floating-point numbers are a finite approximation of real numbers, they are therefore prone to accuracy problems due to the accumulated round-off errors. Concerning the numerical accuracy, parallelism introduces additional problems due to the order of operations between several computation units. Rather than focusing on balancing the load, we focus here on a proper split of the problem driven by the numerical accuracy of the computation. In this paper, we describe a new technique that relies on static analysis by abstract interpretation, and which aims at improving the numerical accuracy of computations by dividing the problem, between computation units, according to the order of magnitude of data.

ABSTRACT. Relational static analyses allow to keep track of the relations between variables in a program. They rely on relational abstract domains like Octagon or Polyhedra. While expressive, these analyses are often costly. To reduce these computations, we design a flow insensitive static analysis that provides a single relational invariant for a whole program. A specific representation of the program, namely the \emph{Static Single Information} (SSI) form, allows us to preserve a good precision (compare to a flow-sensitive analysis) thanks to the indexing of the variables. We report on the design and the soudness of the analysis, using an abstract interpretation methodology. A prototype has been developped to test the usefulness of the analysis on small programs.

ABSTRACT. The Abstract Interpretation framework provides invaluable guidance for the design of abstract domains to be used in static analysis tools. Nonetheless, the development of an adequate abstract domain can be a challenging task: besides the mandatory correctness requirements, also its precision and efficiency need to be properly considered. Drawing mainly from past experience, we show a few examples of the problems that an abstract domain developer may be facing. We rediscuss the tradeoffs that could be adopted while working through the solutions, somehow confirming known rules of thumb, possible exceptions to the rules of thumb and other interesting relationships between correctness, precision and efficiency.

ABSTRACT. Safety-critical embedded software has to satisfy stringent quality requirements. For example, one such requirement, imposed by the relevant safety standard (ISO26262), is that no critical run-time errors must occur. In the last years, we introduced sound static analysis methods and tools in the development process for large-scale software with several million lines of code. They are used to prove highly automated the absence of run-time errors – especially caused by integration. The talk will report on this experience and give an outlook about future challenges.

ABSTRACT. This paper investigates the use of abstract domains from Abstract Interpretation (AI) in the field of Constraint Programming (CP). CP solvers are generally very efficient on a specific constraint language, but can hardly be extended to tackle more general languages, both in terms of variable representation (discrete or continuous) and constraint type (global, arithmetic, etc.). For instance, linear constraints are usually solved with linear programming techniques, but non-linear ones have to be either linearized, reformulated or sent to an external solver. We approach this problem by adapting to CP a popular domain construction used to combine the power of several analyses in AI: the \emph{reduced product}. We apply this product on two well-known abstract domains, Boxes and Polyhedra, that we lift to constraint solving. Finally we define general metrics for the quality of the solver results, and present a benchmark accordingly. Experiments show promising results and good performances.