A collection of Linux kernel configurations for LITMUS^RT kernels used at MPI-SWS (and previously at UNC).
The Coq development for Iris. [project website] [coqdoc]
A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.
The main Coq development of the Prosa project: http://prosa.mpi-sws.org
Model checker for distributed systems using hitting families of schedules
The Coq development of LambdaRust
The main Coq development.
The Coq development for Iris
Logically Atomic Triples in Iris
An extended "Standard Library" for Coq. [coqdoc]
3D visualization of asynchronous program executions.