Explore projects

A logic for proving contextual refinements [project website]

A survey of research papers published at systems conferences, to ascertain the role of visualization in the work, and the extent visualization is presented in the published works.

Iris with transfinite step-indexing

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

Website for SOSP2021 (http://sosp2021.mpi-sws.org)

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

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

A logic for proving contextual refinements [project website]

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

The Coq development of LambdaRust

Model checker for distributed systems using hitting families of schedules

The main Coq development.

The Coq development for Iris

Logically Atomic Triples in Iris