A tool that helps instrumenting a system for distributed tracing. The tool detects places where trace context propagation is potentially needed.
Iris with transfinite step-indexing
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 for Iris
The main Coq development.
The implementation for checking linearizability using hitting families of schedules
PCTCP (Probabilistic Concurrency Testing with Chain Partitioning) algorithm for testing Cassandra system.
Implemented on top of SAMC/DMCK distributed system model checking tool.