Explore projects

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]

Analysis of type classes for Backpack, part of Scott Kilpatrick's PhD thesis. Library for determining the worlds of type class knowledge that modules have. Also a binary, orphans-stats, to compute statistics about orphan instances.

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

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.

Code for computing sufficient, implementable and permissive assumptions.

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

The public repository of the paper "Interactive Programming for Parametric CAD".

Integrates programming and direct manipulation for CAD.

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

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

Maintainer: Felix Stutz

Instrumented version of Cassandra

A verifier for approximations of transcendental functions.

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

The Coq development of LambdaRust

Some example verification demonstrating the use of Iris.

Some example verification demonstrating the use of Iris.