Explore projects

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

The Coq development of LambdaRust

Publicly released Azure Functions traces from https://github.com/Azure/AzurePublicDataset/blob/master/AzureFunctionsDataset2019.md

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

The implementation for checking linearizability using hitting families of schedules

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

The Coq development of LambdaRust

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

Some example verification demonstrating the use of Iris.

Code and documents for "Resilient Abstraction-Based Controller Design"

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

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

Some example verification demonstrating the use of Iris.

Hadoop, YARN, and HDFS, instrumented with tracing framework. Up to date with version 2.7.2. Most up to date branch is brownsys-tracingplane-2.7.2

A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)

ZooKeeper instrumented with tracing framework. Quite out of date (last touched 2014)

HBase instrumented with tracing framework.