Formalisations in Coq
Several of our research results are formalised in the Coq theorem prover. This not only gives us extremely high confidence in the correctness of the results by ruling out the possibility of errors in the proofs, but also makes the results more easily extensible as one can build on our existing formalisations.
Soundness proofs
- Relaxed separation logic (RSL) soundness proof
[Browse] [Browse Full] [Webpage] - GPS soundness proof
[Browse] [Browse Full] [Webpage] - Fenced separation logic (FSL) soundness proof
[Browse] [Browse Full] [Webpage] - Soundness proof of a technique for proving lock-freedom
[Download] [Webpage] - Featherweight VeriFast soundness proof [Download] [Webpage]
Weak memory models
- Correctness of program transformations under the C11 memory model
[Browse] [Browse Full] [Webpage] - The strong release acquire (SRA) memory model
[Browse] [Browse Full] [Webpage]
Compositional compiler correctness
- The SepCompCert verified compiler
[Download] [Webpage] - The Pilsner and Zwickel verified compilers
[Download] [Webpage]
Other
- A memory model for (sequential) C supporting integer-pointer casts
[Download] [Webpage] - A fault-tolerant semantics for pure language with fork-join parallelism
[Download] [Webpage] - A category theory library using Coq 8.5 features
[Browse] [Download] [Paper] - A library for solving recursive domain equations, based on category theory
[Browse] [Download] [Paper]