Programme

Nous introduisons une définition de la dépendance en un point d’un  programme  de la valeur d’une variable à l’égard des valeurs initiales d’une commande pour une sémantique  de traces. Ceci induit une abstraction qui permet de concevoir par calcul une analyse statique  de dépendance structurale et correcte.

Les exigences fonctionnelles d'un système expriment les fonctions que le  système doit réaliser, sans détailler comment les réaliser; en d'autres  termes, elles portent sur le QUOI et et non sur le COMMENT.

Dans le domaine industriel des systèmes temps-réels, de nombreux logiciels ont  pour but d'outiller le développement des spécifications; la plupart se  focalisent sur la gestion et la traçabilité des exigences, mais très peu  apportent une aide efficace pour valider les exigences. L'enjeu pratique est  pourtant important: plus de la moitié des erreurs détectées en phase de test
sont dues à des erreurs de spécifications !

Fondé sur les principes des langages synchrones ainsi que les techniques de  génération de test du laboratoire VERIMAG, le logiciel Stimulus a pour  ambition d'adresser ce problème en permettant de simuler des exigences  modélisée dans un langage formel intuitif mais puissant. Cette capacité de  simulation permet de détecter rapidement les exigences incorrectes, incomplètes ou même contradictoires.

Nous expliquerons comment Stimulus s'intègre dans les processus de  développement existants et illustrerons la modélisation et la mise au point  d'exigences.

Worst-Case Execution Time analysis is mandatory for reactive systems. In this  talk I will show how the properties of reactive systems may help to refine  WCET estimation, how reactive systems environment model may help to get an  idea on the possible execution time and how the implementation of a Lustre  program on a multi-core has been done by combining code generation and timing  analysis.

 

2-adic numbers can be roughly defined as infinite sequences of 0 and 1. The Lustre language and its tools are therefore an convenient platform  to explore these numbers and their algebra.  In particular, the (old) Lustre-to-automaton compiler can be used to  literally "solve" 2-adic equations. We will see that, unsurprisingly,  2-adics encompass natural and relative integers, but also stranger  numbers such that ``one-third'', or ``square root of minus seven''.

Cousot & Halbwachs (1978) proposed inferring convex polyhedra (solution  sets of linear inequalities and equalities) as inductive invariants for  proving properties of program. Their inference process is incomplete: it  may fail to identify convex polyhedra suitable for proving the desired  property even though such polyhedra exist.

The algorithms used in most libraries for computing over convex  polyhedra are based on the double description of polyhedra both as  solution sets of inequalities and equalities, and convex hull of  vertices, rays and lines; the latter description is exponential in the  dimension (the number of variables of the program under analysis) in the  common case where the polyhedron is a distorted hypercube.

Because of these high costs, convex polyhedra were rarely used in static  analysis: often, some restricted subclasses with lower computational  complexity were used, such as products of intervals, difference-bound  matrices, "octagons", or, more generally, template linear constraints  (convex polyhedra with faces along a fixed list of directions).  Furthermore, in these domains, it is possible to make the analysis  complete in the sense that if an inductive invariant suitable for  proving the property exists in the domain, the analysis will find one  (e.g. by computing the strongest inductive invariant in the domain).

At VERIMAG in the past 6 years we have investigated algorithms for  computing over convex polyhedra using constraints only. The first  generation of our algorithms was based on optimized Fourier-Motzkin  elimination, the second generation uses parametric linear programming.  These algorithms are implemented in our library VPL.  https://github.com/VERIMAG-Polyhedra/VPL

Is analysis with general convex polyhedra necessarily incomplete? I have shown the existence of inductive convex polyhedral invariants to be  undecidable, but using some nonlinear (polynomial) transitions. The question remains open using only linear transitions.

Linear Relation Analysis, or polyhedral abstract interpretation, is one of the  first applications  of abstract interpretation and still one of the most powerful numerical  relational analyses.
We designed a new modular analysis, computing disjunctive relational summaries,  to improve the scalability of Linear Relation Analysis.  We show how it is applied to the analysis of programs with procedures, objects  and synchronous modules.

Authors: Albert Benveniste et Thierry Gautier, Inria Rennes

Abstract: The synchronous language Signal is part of the french family of  synchronous languages, yet it has an original positioning in it. It addresses  open systems and architectural aspects. Clocks are therefore at the heart of  the language. Clocks are handled as types and are synthesized, not verified (as  in Lustre). We will focus our presentation on the very principles of Signal,  namely its clock and causality calculus. We will show how these principles  naturally extend to physical system modeling based on first principles of the  physics, handled as constraints, not functions. This exrension of Signal is
kind of a discrete time counterpart of the Modelica language.

This talk will address the technologies used to develop the flight  software controlling the European Ariane 6 launcher as well as the associated challenges.

Proving the absence of bugs in a given software is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations.

Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers).

In this talk I will present some experiences in the design of scalable static analyses inside compilers, and try to make a synthesis about the general framework we, together with my coauthors, used to develop them. I will also show some experimental evidence of the impact of this work on real-world compilers, as well as future perspective for this area of research.