Iris - Une logique de séparation d'ordre supérieur implémentée dasn l'assistant de preuve Coq
Date de dernière version : 18 décembre 2017

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

CODALAB
open source framework for running competitions

DNADNA
Deep Neural Architectures for DNA

CARTOLABE
CARTOLABE