Explore projects

A logic for proving contextual refinements [project website]

Some example verification demonstrating the use of Iris.

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

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

ns3 simulations for different congestion control algorithms and network scenarios.

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.

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

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

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

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

This project contains some scripts and other files that are used by many Iris project for their CI

DeathStarBench modified with X-Trace tracing

A simulator to visualize/analyze tracking data from VR

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