Explore projects

The Iron logic for precise reasoning about resources [project website]

Unmaintained repository. See here for a maintained fork.

Formalizes the ordered RA model of Iris from the MoSeL paper

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

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

A modified version of StochasticSynthesis that we used for our TAC '21 and TACAS '22 submissions. The original repo is here: https://github.com/gtfactslab/StochasticSynthesis

A tool that helps instrumenting a system for distributed tracing. The tool detects places where trace context propagation is potentially needed.

A Programming and Direct Manipulation Environment for creating test environments/scenarios, especially for the case of Autonomous Driving.

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

Logically Atomic Triples in Iris

An extended "Standard Library" for Coq. coqdoc(https://plv.mpi-sws.org/coqdoc/stdpp/)

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

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

This is the repository for the EU EIC project called SymAware.

A simulator to visualize/analyze tracking data from VR

The main Coq development.