Iris - A Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.


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/

- Licence : BSD License



Research activities
  Deductive Verification of Programs

Members
  JOURDAN Jacques-Henri

Group
  Verification of Algorithms, Languages and Systems

BSP++
The C++ Bulk Synchronous Parallelism Library

TAXOMAP ALIGNMENT
A prototype to automate semantic mappings between taxonomies

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