Explore projects

A logic for proving contextual refinements [project website]

Models compiled for use with Clockwork on MPI volta machines (tesla v100)

Mirror of https://github.com/dmlc/tvm for internal development

Check other branches for active development.

Don't forgot to git submodule init and git submodule update!

Some example verification demonstrating the use of Iris.

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

Barebones C++ implementation of X-Trace compatible with latest brown tracing framework + baggage version

Barebones C++ implementation of X-Trace compatible with latest brown tracing framework + baggage version

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

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

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

ns3 simulations for different congestion control algorithms and network scenarios.

Some example verification demonstrating the use of Iris.

Java implementation of tracingplane and baggage

A collection of Linux kernel configurations for LITMUS^RT kernels used at MPI-SWS (and previously at UNC).

Practical verification of numerical kernels

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

Some example verification demonstrating the use of Iris.

An "Iris plugin" to add support for Gallina names in intro patterns to the Iris Proof Mode

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