Fran├žais Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software Iris
Iris - A Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.
Date of the last release: 18 December 2017

Person in charge : JOURDAN Jacques-Henri


Iris is a Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq. It can be used for reasoning about safety of concurrent programs, as the logic in logical relations, to reason about type systems, etc. Iris is developed at LRI, jointly with MPI-SWS (Germany), the Delft University of Technology (Pays-Bas) and with the Aarhus University (Denmark).

More information: http://iris-project.org/

Software - Licence : BSD License



Research activities
  Deductive Verification of Programs

Members
  JOURDAN Jacques-Henri

Group
  Verification of Algorithms, Languages and Systems

Software & patents
CODALAB
Codalab

DNADNA
Deep Neural Architectures for DNA

CARTOLABE
CARTOLABE