Projet ANR-11-BS02-0016 – CLIMT : Méthodes catégoriques et logiques en transformations de modèles
Programme : Blanc - SIMI 2 - Science informatique et applications (Blanc SIMI 2) 2011
Année de financement : 2011
Coordinateur du projet : Monsieur Rachid ECHAHED (CNRS - DELEGATION REGIONALE RHONE-ALPES SECTEUR ALPES)
Partenaires : Laboratoire d'Informatique de Grenoble; Institut de Recherche en Informatique de Toulouse
Montant : 320000.0 euros
Durée : 48 mois
Résumé : Il existe de nombreuses manières d'aborder le problème de la qualité
des logiciels. Le spectre de ces techniques s'étend des obligations de
preuves, des conceptions d'architecture, des langages de
spécifications, des langages de programmation jusqu'au test et à la
vérification de programmes. Ces méthodes sont souvent  spécifiques à
un paradigme de programmation donné. La programmation déclarative à
base de règles est une des approches abstraites parmi les plus
prometteuses pour l'amélioration de la productivité et de la qualité
du logiciel.
La programmation basée sur des règles permet en général
une meilleure lisibilité, écriture et maintenance du logiciel. Quand les
règles opèrent sur des objets représentés par des arbres (ou des
chaînes de caractères), beaucoup de techniques de vérification de
programmes ont été proposées dans la littérature renforçant
considérablement la qualité du logiciel. Cependant de nombreux
problèmes pratiques ne peuvent être encodés facilement sous
forme d'arbres. Ces problèmes nécessitent l'utilisation de structures
plus élaborées comme les graphes. Les graphes sont des objets
mathématiques très communs, visuellement parlant et intuitifs. Ils
constituent une approche naturelle de la modélisation qui est utilisée
dans de nombreux domaines scientifiques comme l'informatique, les
sciences du vivant, l'économie ou la sociologie.
L'objectif du projet CLIMT consiste en le développement de nouveaux
formalismes de haut niveau afin de donner des bases théoriques, facilitant
la vérification de programmes basés sur des règles opérant sur des structures
de données complexes modélisées par des graphes. A cette fin nous
allons organiser notre recherche selon les trois axes suivants~:
  (i)Le premier consiste en l'étude  de nouvelles classes
  de système de réécriture de graphes avec une attention particulière
  portée sur de nouveaux traits  comme le clonage ou l'utilisation d'attributs 
  inductifs.
  (ii)Le second axe de recherche consiste en la définition de
  nouvelles logiques et techniques de preuves pour exprimer et
  réaliser de manière semi automatique des preuves de correction et de
  propriétés des systèmes de réécriture considérés.
  (iii) Dans le troisième axe, nous étudierons des techniques de
  preuves dont le but est d'améliorer l'espace de recherche des
  systèmes d'aide à la preuve des systèmes de réécriture de
  graphes. Ceci se fera par exemple en faisant appel à des procédures
  spécialisées (SAT ou SMT) ou en utilisant des techniques de
  détection de symétrie afin d'éviter les redondances.
Ce projet sera une opportunité de réunir des expertises
complémentaires dans les domaines de la transformation de graphes,
des systèmes de preuve automatique, de la logique pour proposer de
nouvelles méthodes formelles, des techniques efficaces et des outils
spécifiques pour le développement et la certification de programmes
basés sur des règles et opérant sur des graphes.