Projects
Relaxed Memory Model Zoo
A living survey of published weak memory models
A living survey of weak memory models: 101 models spanning 47 years — hardware, programming language, distributed and transactional — and 145 relations between them, ordered by the inclusion of the behaviours they allow. Every ordering claim states how it is known, and 65 herd7 litmus tests run on every push.
MoRDor
Symbolic weak memory analysis for C-like programs
A CLI and web UI for weak memory analysis of C-like programs, and the reference implementation of Symbolic Modular Relaxed Dependencies (sMRD): it parses litmus tests, calculates symbolic dependencies between memory operations, decides episodicity of unbounded loops, visualises event structures and executions, and runs symbolic verification.
Isabelle Automation
Python tooling for automated theorem proving in Isabelle
Python packages for driving the Isabelle theorem prover from code: a Language Server Protocol client, an Isabelle client on top of it that reads the proof state at any point of a theory and can replace proof steps, a parser that turns Isabelle/Isar theory files into parse trees without running Isabelle, and an incremental checker that lets agents re-check only what they changed.