Explore projects

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

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

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

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

A survey of research papers published at systems conferences, to ascertain the role of visualization in the work, and the extent visualization is presented in the published works.

Some example verification demonstrating the use of Iris.

An extended "Standard Library" for Coq. coqdoc(https://plv.mpi-sws.org/coqdoc/stdpp/)

PCTCP (Probabilistic Concurrency Testing with Chain Partitioning) algorithm for testing Cassandra system. Implemented on top of SAMC/DMCK distributed system model checking tool.

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

opam repository for old versions of things we develop (to avoid accumulating too many versions in the main repository)

Some example verification demonstrating the use of Iris.

A new, nondeterministic floating-point source semantics and a proof-of-concept connection to the CakeML verified compiler.

A logic for proving contextual refinements [project website]

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.