Patrick Cousot, Analyse statique de dépendance par interprétation abstraite

Patrick Cousot.
Analyse statique de dépendance par interprétation abstraite
Journée en l'honneur de Nicolas Halbwachs, (Nicolas Halbwachs's Fest), Grenoble, France, Lundi 4 juin 2018.
Slides of the 55mn presentation at Nicolas Halbwachs's Fest (in French):
- US letter, 1 slide per landscape page, 316 Kb,
- A4, 4 slides per landscape page, 638 Kb,
Résumé:
   La notion de dépendance intervient dans de nombreux raisonnements sur les programmes : non-interférence (confidentialité, intégrité); sécurité, vie privée; découpage de programmes (slicing), dépendances temporelles en Lustre, Signal, et autres langages synchrones; etc.
   Les définitions existantes sont données à priori et, à quelques exceptions près, sans justifications sémantiques. De plus les définitions sémantiques existantes sont inutilement compliquées ou réduites à des cas particuliers (par exemple les dépendances sont observées à la fin du programme pas en cours d'exécution).
   Notre objectif est de montrer le principe de la définition sémantique formelle de dépendance par interprétation abstraite et de la dérivation constructive par calcul d'un algorithme d'analyse de dépendance correct, pas d'obtenir une nouvelle analyse de dépendance plus puissante.
   Nous introduisons une définition formelle de la dépendance en un point d'un programme de la valeur d'un variable en fonction des valeurs initiales des variables 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. Parmi les abstractions possibles, notre choix se porte sur l'analyse d'une variante de Denning et Denning (1977), localement plus précise.
Abstract:Dependency is a basic concept occurring in many reasonings on programs: non-interference (confidentiality, integrity); security, privacy; slicing; temporal dependencies in synchronous languages like Lustre and Signal, etc.
   Existing definitions are given a priori and, apart from very few exceptions, without semantic justifications. Moreover the existing semantic definitions of dependency are uselessly complicated or particular cases (such as dependencies observed at the end of the program, not during execution).
    Our objective is to show the principle of a formal semantic definition of dependency by abstract interpretation and the constructive derivation of a sound dependency analysis algorithm, not to obtain a new more powerful static analysis.
   We introduce a formal definition of dependency of the value of a variable at a program point of a statement upon the initial values of the variables at that statement for a trace semantics. This induces an abstraction allowing us to design by calculus a structural sound dependency analysis. Among the possible abstractions, our choice is to derive a variant of Denning and Denning (1977), locally more precise.
Mots-clés:
Méthodes formelles, Sémantique, Propriété de programme, Dépendance, Absence d'interférence, Abstraction, Interprétation abstraite.
Keywords:
Formal methods, Semantics, Program property, Dependency, Non-interference, Abstraction, Abstract interpretation.

Bibliographic reference:

@inproceedings{CousotHalbwachsFest2018,
  author    = {Patrick Cousot},
  title     = {Analyse statique de dépendance par interprétation abstraite},
  booktitle = {Journée en l'honneur de Nicolas Halbwachs, Grenoble, France, Lundi 4 juin 2018},
  year      = {2018},
  publisher = {{VéRIMAG, Université Grenoble Alpes (France)}},
  url       = {https://nhalbwachs2018.sciencesconf.org},
}

\bibitem{CousotHalbwachsFest2018}
Patrick Cousot.
\newblock Analyse statique de dépendance par interprétation abstraite.
\newblock In \emph{Journée en l'honneur de Nicolas Halbwachs, Grenoble, France, Lundi 4 juin 2018}, 
          VéRIMAG, Université Grenoble Alpes (France), Grenoble, France, Lundi 4 juin 2018.
          (\url{{https://nhalbwachs2018.sciencesconf.org}}

copyright notice
Last modified: Tue Jun 5 18:46:32 CEST 2018