Iris - Une logique de séparation d'ordre supérieur implémentée dasn l'assistant de preuve Coq
Date de dépôt : 01 janvier 1970

Responsable : JOURDAN Jacques-Henri


Iris est une logique de séparation d'ordre supérieur implémentée dans l'assistant de preuve Coq. Elle peut être utilisée pour prouver la sûreté de programmes concurrents, pour construire des relations logiques, pour démontrer la sûreté de systèmes de types, etc... Iris est développée au LRI, conjointement avec le MPI-SWS (Allemagne), avec la Delft University of Technology (Pays-Bas) et avec l'Aarhus University (Danemark).

Pour en savoir plus: http://iris-project.org/

Logiciel - Licence : BSD License



Activités de recherche
  Vérification déductive de programmes

Membres
  JOURDAN Jacques-Henri

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

BSP++
The C++ Bulk Synchronous Parallelism Library

TAXOMAP ALIGNMENT
Un outil d'alignement de taxonomies

FR1155729
Procédé pour l’extinction de routeurs dans un réseau de communications et routeur mettant en œuvre ce procédé