Previous Up

Lot 5 : technologie de vérification

Sous-lot 1 : ajouter la réécriture au noyau de calcul de Coq

Disponible
  • définition de la classe de réécriture à intégrer ps pdf
  • proposition d'architecture du moteur de test de conversion ps pdf
  • prototype d'extension du système Coq ps pdf
  • combinaison à des systèmes de vérification automatique de terminaison ps pdf.
La fourniture suivante est annulée et compensée par une étude plus approfondie de la preuve par réécriture probabiliste, lot 4.2
  • validation du prototype sur des exemples

Sous-lot 2 : vérification compositionnelle

Les fournitures suivantes sont annulées et compensées par le renforcement du sous-lot 2, contributions LSV F4.2.2 et F4.2.3

  • prototype d'extension du système de model-checking compositionnel HCMC aux p-automates
  • validation du prototype sur des exemples tels que PGM avec un nombre significatif d'émetteurs et récepteurs
  • utilisation de techniques de preuve interactive entre HCMC et Coq

Sous-lot 3 : mécanisation de la déduction

Disponible
  • coopération Coq/ELAN pour la recherche et la vérification de preuves de théorèmes équationels ou inductifs ps pdf
  • description d'une méthode de preuve pour les inductifs du premier ordre ps pdf
  • utilisation des techniques de narrowing pour la recherche des schémas de récurrence cette fourniture est une extension de celle qui était prévue auparavant sous le même titre, de sorte que les résultats obtenus, bien qu'ils soient finalement orientés, différemment, couvrent sous une forme qui nous paraît plus utile le volume de travail prévu pour la dernière fourniture (initialement, celle-ci devait porter sur les preuves par consistance) pdf
A FAIRE : explication à compléter
  • implantation et validation de la méthode sur des exemples

Previous Up