Explore projects

Raw Jaeger traces and X-Trace converted traces of DeathStarBench executions

A simple dataset of traces of the Hadoop Distributed File System (HDFS).

The implementation for checking linearizability using hitting families of schedules

The main Coq development.

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

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

An extended "Standard Library" for Coq

This is a static analyser developed for the Program Analysis course at TU Kaiserslautern. for more information see the course page: https://moodle.mpi-sws.org/course/view.php?id=24

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

UniTraX is a data analytics system that provides users with a personal differentially private bound on privacy loss. UniTraX is able to allow more queries than previous systems, without giving up on analytic accuracy.

UniTraX data for experiments. See main repository at https://gitlab.mpi-sws.org/anon/unitrax for more information.

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

Some example verification demonstrating the use of Iris.

Exercises for the Iris tutorial

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.

Generative Models are being developed currently which can potentially be used for various applications such as data generation for training models. This project aims to analyse a generative model, the Variational Autoencoder and potential bias in it.

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