Abstract FR:

Nous presentons quatre resultats en semantique et analyse automatique de programmes (1) un algorithme de determination statique de proprietes de partages (aliasing) de donnees allouees dynamiquement dans des langages stricts, a portee lexicale, avec operations imperatives et continuations de premiere classe d'ordre superieur ; (2) le treillis des relations monomiales unitaires-prefixes sur un langage regulier, qui generalise la decomposition structurelle d'eilenberg et la decomposition de parikh et peut etre utilise pour representer finement des relations arbitraires sur un langage, y compris des relations algebriques ; (3) un modele des langages de programmation polymorphes avec operations imperatives base sur des relations d'equivalence regulieres a droite entre chemins d'acces de donnees, des algorithmes globaux et on-line bases sur ce modele et sur le resultat n 2 de determination statique de proprietes d'aliasing uniformes et non-uniformes de donnees structurees allouees dynamiquement dans des langages a typage polymorphe ; ces algorithmes ont ete prouves corrects en utilisant l'interpretation abstraite comme cadre theorique et valides experimentalement par un prototype pour un fragment d'ordre un du langage ml ; les applications comprennent l'optimisation statique de la gestion de la memoire dynamique, la verification statique de non-interference et l'analyse de dependances pour des langages paralleles ; (4) un modele operationnel de proprietes de strictness, et bases sur ce modele et sur le resultat n2, des algorithmes on-line de determination statique de proprietes de strictness dans des langages avec appel par necessite