Logiciels et Brevets (Production scientifique) - Laboratoire de Recherche en Informatique

Logiciel Coccinelle

Coccinelle - Coccinelle
Date de dernière version : 01 janvier 2014

Responsable : CONTEJEAN Evelyne

Le but général de cette bibliothèque est d'utiliser le démonstrateur
automatique CiME pour produire des preuves en Coq, entre autres :

d'égalité modulo dans une algèbre de termes quotient,
de terminaison d'un système de réécriture,
de confluence locale d'un tel système,
de convergence.

Pour en savoir plus: http://www.lri.fr/~contejea/Coccinelle/coccinelle.html

Logiciel

Activités de recherche
  Démonstration automatique
  Réécriture

Membres
  CONTEJEAN Evelyne

Equipe
  Vérification d'Algorithmes, Langages et Systèmes