Projet ANR-10-JCJC-0203 – AMIS : Méthodes algorithmiques pour les graphes infinis
Programme : JCJC : Sciences de l'information, de la matière et de l'ingénierie : Sciences de l’information, simulation (JCJC SIMI 2)
Année de financement : 2010
Coordinateur du projet : Monsieur ARNAUD CARAYOL (UNIVERSITE PARIS-EST MARNE LA VALLEE)
Partenaires : Laboratoire d'Informatique Gaspard-Monge
Montant : 103160.0 euros
Date de début : 2011
Durée : 36 mois
Résumé : Vérification de programmes fonctionnelsLe projet AMIS est un projet de recherche fondamentale coordonné par Arnaud Carayol. Il associe aussi Christopher Broadbent, Axel Haddad, Matthew Hague, Antoine Meyer, Chloé Rispal et Oliver Serre. Le projet a commencé en janvier 2011 et a duré 36 mois. Il a été intégralement financé par une aide ANR de 103160 €.
Modéliser les programmes et systèmes informatiques pour en vérifier les propriétésLa complexité du monde ne permet pas de prédire avec exactitude son comportement. Il faut donc concevoir des modèles, des abstractions suffisamment fidèles pour tenter de le comprendre. En informatique, il est parfois indispensable de garantir le respect par un programme de ses spécifications, si possible automatiquement. Des modèles de programmes, comme la machine de Turing ou le ?-calcul de Church, existent depuis la création de notre discipline, mais leur vérification automatique (c’est-à-dire par une machine) se heurte au problème de l’indécidabilité. Dès lors, il est naturel de considérer des modèles de calcul plus simples, dont la vérification automatique est possible mais qui restent assez expressifs pour représenter des aspects intéressants de programmes réels. La principale contribution de ce projet fut de mettre au point un outil de vérification automatique de programmes dits fonctionnels, dont la particularité est d’autoriser les fonctions à admettre comme paramètres (ou à produire comme résultat) d’autres fonctions. De nombreux langages de programmation comme CaML, Python, C++, C# ou Java ont été conçus ou enrichis avec ces aspects.
Vérification de programmes fonctionnels à l’aide de machines à effondrementLe résultat d’indécidabilité déjà mentionné ne permet pas d’envisager la vérificationd’un programme fonctionnel tel qu’il est exécuté par un ordinateur. Il est nécessaire d’en donner un modèle abstrait qui en simplifie certains aspect. Les schémas récursifs d’ordre supérieur (ou plus simplement schémas de programmes) fournissent une abstraction fidèle des programmes fonctionnels. Des résultats dûs à Ong en 2006 montrent que de nombreuses propriétés de ces modèles sont vérifiables. Deux tâches se présentent alors : réaliser des outils efficaces (c’est à dire permettant de traiter des programmes de taille conséquente) et aller au delà de la simple validation pour corriger automatiquement un code existant. Plusieurs vérificateurs ont été développés ces dernières années pour vérifier les propriétés des schémas récursifs d’ordre supérieur. Dans ce projet, nous avons adopté une approche consistant à transformer un schéma de programme en une machine à espace d’états fini appelée automate à effondrement. Cette étape intermédiaire permet de profiter de la riche théorie des automates finis et infinis.
Résumé de la soumission : L'apparition de la technique dite de "model-checking à états finis" a constitué l'une des avancées significatives vers la vérification automatique de systèmes informatiques. Cet ensemble de techniques apparues il y a une trentaine d'années est aujourd'hui devenue répandue et reconnue. Sa spécificité est de représenter le système étudié par un automate fini, et de répondre à diverses requêtes sur le système réel grâce à des techniques algorithmiques classiques sur les graphes finis. Cette approche est particulièrement pertinente pour l'analyse de systèmes dits à espace d'états fini, tels les circuits matériels ou certains protocoles de sécurités, car ce modèle formel est suffisamment expressif pour représenter fidèlement l'essentiel des comportements de tels systèmes.Les systèmes plus complexes, comme par exemple les logiciels modernes, présentent souvent un ou plusieurs aspects infinis, ou du moins non bornés, tels que la récursion, le parallélisme, la présence de structures de données non bornées, etc. Pour raisonner sur de tels systèmes à nombre infini d'états, les chercheurs ont du développer des modèles formels plus expressifs en mesure de prendre en compte tout ou partie de ces aspects complexes.Dans ce projet, nous nous intéressons particulièrement au traitement de la récursion. Dans ce contexte, les systèmes les plus élémentaires sont les programmes séquentiels récursifs sur des domaines de données bornés, par exemple des programmes en C à fonctions récursives mais sans manipulation de pointeurs. Le comportement de tels programmes peut être fidèlement représenté à l'aide d'automates à pile, en utilisant la pile de l'automate pour stocker les informations relatives aux appels successifs de fonctions. Plusieurs équipes de recherche ont exploité cette idée pour proposer des méthodes et outils efficaces de vérification de programmes récursifs.Nous souhaitons nous appuyer sur les modèles existants de programmes séquentiels récursifs et explorer le cadre plus riche de la récursion d'ordre supérieur, où les arguments passés à des fonctions ne sont plus limités à des valeurs simples mais peuvent être eux-mêmes des fonctions. Parmi les modèles abstraits connus permettant de représenter de tels programmes figurent les schémas récursifs d'ordre supérieur, ainsi que les automates à pile d'ordre supérieur et automates effondrants. Des résultats récents sur ces objets en on fait l'un des thèmes actuels principaux dans notre communauté, mais de nombreuses questions restent à l'heure actuelle ouvertes.
Résultats : Le projet AMIS a permis de réaliser un outil de vérification de schéma de programme appelé C-Shore.  Cet outil a des performances comparables aux autres vérificateurs et permet de traiter des programmes d’une cinquantaine de lignes. Nous avons pu ainsi valider l’approche basée sur la théorie des automates finis. De plus nous avons établi les résultats théoriques qui permette d’envisager de passer de la vérification de programmes à la synthèse de programmes à partir de leur spécifications.
Perspectives : Un des buts initiaux de nos travaux était de développer un langage d'entrée pour C-SHORe. Le langage serait idéalement plus proche d'un langage de programmation existant que des schémas de récursion et se traduirait naturellement en schéma de récursion.
A l'exception de modifications mineures pour ajouter les disjonctions de cas aux schémas de récursions, nous n'avons pas pu développer cette piste.
L'étude du langage d'entrée est l'une de nos principales piste de recherche.
Enfin même si,  nous avons mis en évidence que notre algorithme de saturation se généralise aux machines à effondrement concurrentes, il reste à développer un algorithme efficace dans l'outil C-SHORe. Dans la même ligne, il nous faudrait implémenter un module de synthèse de programme à notre outil.
Publications et brevets : La réalisation de l’outil C-Shore a donnée lieu à l’écriture d’une dizaine d’articles dans des conférences internationales prestigieuses (comme ICALP, LICS ou ICFP). Parmis les 
contributions théoriques notables, nous avons simplifiés la traduction de schémas 
de programmes en machine à effondrement et développé un algorithme basé sur des méthodes de saturations pour la vérification des machines à effondrement.