The group for Iris and projects related to it. The core repository here is Iris itself.
Unmaintained repository. A monadic translation of mini C into Iris's HeapLang [project website]
This project contains some scripts and other files that are used by many Iris project for their CI
Automation for Iris
Some example verification demonstrating the use of Iris.
Unmaintained repository. An extension of the Iris program logic to support linearity and fair refinement reasoning.
A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)
The Coq development for Iris. [project website] [coqdoc]
The Iron logic for precise reasoning about resources [project website]
The Coq development of LambdaRust
opam repository for development versions of things we develop.
opam repository for old versions of things we develop (to avoid accumulating too many versions in the main repository)
Unmaintained repository. See here for a maintained fork.
Formalizes the ordered RA model of Iris from the MoSeL paper
Operational Repaired C11
