A tool that helps instrumenting a system for distributed tracing. The tool detects places where trace context propagation is potentially needed.
A certificate checker for roundoff error bounds
Some example verification demonstrating the use of Iris.
A verifier for approximations of transcendental functions.
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]
The Coq development of LambdaRust
The main Coq development.
The Coq development for Iris