Explore projects

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

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

Safety of a syntactically unsafe symbol ADT.

Deprecated repository; please use the POPL 2021 version instead

This repo contains our prototype implementing the generalised projection of global types from our MST framework with generalised choice.

Maintainer: Felix Stutz

Prototype gRPC server with a customizable topology; principally used for Hindsight evaluation.

PCTCP (Probabilistic Concurrency Testing with Chain Partitioning) algorithm for testing Cassandra system. Implemented on top of SAMC/DMCK distributed system model checking tool.

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

The Coq development of LambdaRust

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

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

Logically Atomic Triples in Iris

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

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

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