Explore projects

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

The Coq development for Iris

The main Coq development.

The Coq development for Iris

The main Coq development.

An extended "Standard Library" for Coq. [coqdoc]

3D visualization of asynchronous program executions.