Explore GitLab
Discover projects, groups and snippets. Share your projects with others

Zhen Zhang / iriscoq
The Coq development for Iris

FP / opamdev
opam repository for development versions of things we develop.
1updated 
FP / LambdaRustcoq
The Coq development of LambdaRust

FP / iriscoq
The Coq development for Iris

RTPROOFS / PROSA  Formally Proven Schedulability Analysis
The main Coq development of the Prosa project: http://prosa.mpisws.org
1updated 
Sergey Bozhko / rtproofs
The main Coq development.
0updated 
Jonas Kastberg / iriscoq
The Coq development for Iris

Pascal Fradet / rtproofs
The main Coq development.
1updated 
FP / irisci
This project contains some scripts and other files that are used by many Iris project for their CI
0updated 
Sophie Quinton / rtproofs
The main Coq development.

Marcus Pirron / CableRobot
Code for the CableRobot

FP / gpfsl
A combination of GPS and FSL in the promising semantics WITHOUT promises

FP / orc11
Operational Repaired C11

FP / promising
An extraction of the promising semantics

FP / ragps
A soundness proof for GPS and RSL with ReleaseAcquire semantics in Iris.

Amin Timany / irisora
Formalizes the ordered RA model of Iris

Joseph Tassarotti / fricoq
An extension of the Iris program logic to support linearity and fair refinement reasoning.
0updated 
Dan Frumin / ReLoC
A calculus of logical relations for concurrency, formalized in Iris.

FP / irisatomic
Logically Atomic Triples in Iris

FP / irisexamples
Some example verification demonstrating the use of Iris.