Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
Logiciel Iris
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

Logiciels et brevets
DNADNA
Deep Neural Networks for DNA

TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas