Explore projects

Some example verification demonstrating the use of Iris.

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

Axiomatic pWCET, formalized in Coq

This is the repository for the EU EIC project called SymAware.

Coq development for the Semantics course taught at Saarland University

Local Simulation proofs, the Iris style

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

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

A logic for proving contextual refinements [project website]

The Iron logic for precise reasoning about resources [project website]

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

https://os.mpi-sws.org/

The Coq development of LambdaRust

The Coq development for Iris. project website(https://iris-project.org/) coqdoc(https://plv.mpi-sws.org/coqdoc/iris/)

Some example verification demonstrating the use of Iris.

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