Explore projects

This project hopes to gather bibliographic sources regarding weak memory.

YCSB is a cloud database benchmark that we use for HBase

Python reference implementations of the real-time model inference algorithms used by LiME

A logic for proving contextual refinements [project website]

The benchmark repository for the added float support to the KeY deductive verifier.

Some example verification demonstrating the use of Iris.

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

Some example verification demonstrating the use of Iris.

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

Coq development for "The High-Level Benefits of Low-Level Sandboxing"

A fork of the Haskell Cabal repository that includes a change necessary for running the Class Struggle analysis, as part of Scott Kilpatrick's PhD thesis.

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

Logically Atomic Triples in Iris

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