APRON

Numerical Program Analysis

This projects belongs to the ACI "Sécurité & Informatique"























































APRON Plenary Meeting

École des mines de Paris, Paris, Sept. 20, 2005



Attendance: Corinne Ancourt (CRI/EMP), Julien Bertrane (ENS), Guillaume Capron (X), Patrick Cousot (ENS), Radhia Cousot (CNRS), Jérôme Feret (ENS), Nicolas Halbwachs (VERIMAG/CNRS), François Irigoin (CRI/EMP), Bertrand Jeannet (IRISA), Francesco Logozzo (ENS), Antoine Miné (ENS), Mathias Péron (VERIMAG/CNRS), Sebastian Pop (CRI/EMP), Élodie-Jane Sims (X)

Excused: Laure Gonnord (VERIMAG/CNRS)

Seven talks were given by members of all participating teams during the day. The list of common cases now includes the CH78 and the car and the car burner cases contributed by Verimag, the deglitcher/debouncer and the raising edge detectiom cases contributed by École polytechnique. École des mines would like to add a lift specification by Boigelot and Wolper.

  • Presentation by Guillaume Capron (École Polytechnique): Vérification de propriétés réactives sur des macro-définitions (the slides are not yet accessible)

    Certains programmes réactifs sont générés automatiquement à partir de macro-définitions. Nous présentons une méthode pour tester si certaines macro-définitions écrites en C respectent leur spécification. Cette dernière définit les propriétés réactives bornées dans le temps. Nous utilisons l'interprétation abstraite et fournissons une formalisation de la spécification, une sémantique et des algorithmes pour nous permettre de construire une représentation compacte des ensembles de traces en utilisant les schémas d'arbres.

  • Exposé de Nicolas Halbwachs sur les travaux de Laure Gonnord (VERIMAG/CNRS): Combinaison d'élargissements et d'accélération en analyse de relations linéaires

  • Presentation by Élodie-Jane Sims (École Polytechnique): Abstraction of $BI^{\mu\nu}$ formulae

    Nous présentons un domaine abstrait pour les formules de la logique de séparation avec points fixes. Il contient des informations de shape et d'aliasing. Pour garder le domaine général, il est paramétré par un domaine abstrait numérique qui peut être instancié par les domaines existants (relationnels ou non). Nous avons une sémantique concrète en terme d'ensemble de mémoires (le même modèle que pour la logique de séparation) et quelques fonctions sur le domaine.

  • Exposé de Francesco Logozzo (ENS): A static analyzer for sequential Java based on Octagons

    We present a static analysis for the analysis of Java classes in isolation. We will discuss our implementation and the underlying model of memory. In particular, we will describe the abstract domain, based on Octagons, that we use for the abstraction of Java memory states. Finally we will discuss some implementation issues (the analyzer is written in Java) and the comparison with (well-known) existing tools.

  • Exposé de Bertrand Jeannet (IRISA): Interface générique APRON pour domaines numériques abstraits,

    Un des objectifs d'APRON est de confronter et de mettre en commun nos techniques et outils. Quelques chercheurs de l'IRISA, du CRI, de l'ENS et de VERIMAG se sont réunis plusieurs fois (1er février, 15 mars, 28 juin) pour jeter les bases d'une interface satisfaisant les besoins exprimés par tous. Le but est de présenter les résultats de nos différentes réunions, les principes dégagés, les perspectives, et faire le point sur le début de mise en oeuvre effectué à Rennes.

  • Exposé de Jérôme Feret (ENS): Analyse statique de filtres numériques,

    Le filtrage numérique est couramment utilisé dans les systèmes temps réels embarqués (par exemple dans l'automobile, l'aéronautique ou l'aérospatiale). Il permet de modéliser au niveau logiciel des comportements (comme la recherche d'équilibre) qui étaient autrefois assurés par des filtres mécaniques (hydrauliques par exemple), puis par des filtres analogiques. Cependant, la modélisation de ces filtres au niveau logiciel peut poser des problèmes, comme par exemple la stabilité du flux de sortie en présence d'arrondis. Notre but est alors de prouver l'absence d'erreurs à l'exécution (essentiellement des débordements de nombres à virgule flottante) dans un programme comprenant du filtrage numérique. Nous utilisons l'interprétation abstraite pour construire des domaines adaptés au filtrage. Nous pouvons ainsi raffiner des analyses existantes pour tenir compte de ces filtres. Nous associons à chaque famille de filtres, un domaine abstrait. Ce domaine est essentiellement une boîte noire, qui associe à l'approximation du flux d'entrée du filtre une approximation du flux de sortie. Le domaine se charge alors de repérer toutes les instances des filtres de cette famille, et d'utiliser les contraintes que l'analyseur a découvert sur les entrées, pour inférer les contraintes sur les sorties de ces filtres. Cette méthodologie a été entièrement incorporé à ASTRÉE (analyseur statique de logiciels temps-réel embarqués).

  • Exposé de François Irigoin: Analyse de programme et analyse d'automate

    L'analyse modulaire implantée dans l'outil PIPS a été mis au point empiriquement pour satisfaire les besoins rencontrés pour des programmes scientifiques. La prise en compte des boucles est faite de manière très simple: aucun élargissement n'est utilisé. Deux questions se posent: 1): pourquoi ceci fonctionne-t-il de manière suffisament précise pour nous? et 2) pourquoi le comportement des automates est-il par contre mal caractérisé par PIPS?