Explore projects

Automation for Iris

This project hopes to gather bibliographic sources regarding weak memory.

SimBricks website source, automatically deployed to https://www.simbricks.io

SimBricks repository mirror, only used for CI. Use https://github.com/simbricks/simbricks

Iris with transfinite step-indexing

opam repository for development versions of things we develop.

Some example verification demonstrating the use of Iris.

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

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

A tutorial for the Iris Separation Logic Framework

The Coq development of LambdaRust

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

A combination of GPS and FSL in the ORC11 semantics (the promising semantics WITHOUT promises)

Local Simulation proofs, the Iris style

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

Axiomatic pWCET, formalized in Coq