The Coq development for Iris. [project website] [coqdoc]

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

The main Coq development of the Prosa project: http://prosa.mpi-sws.org

Safety of a syntactically unsafe symbol ADT.

The main Coq development.

A custom Akka dispatcher that logs and controls the delivery order of actor messages.

OLD VERSION, SEE https://gitlab.mpi-sws.org/iris/reloc INSTEAD

A soundness proof for GPS and RSL with Release-Acquire semantics in Iris.

DeathStarBench modified with X-Trace tracing

Exercises for the Iris tutorial at POPL 2018

The Coq development of LambdaRust

opam repository for development versions of things we develop.

Practical verification of numerical kernels

Model checker for distributed systems using hitting families of schedules

The main Coq development of the Prosa project: http://prosa.mpi-sws.org