|
|
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
|
|
|
|
|
