Category:

Verifying C11-style weak memory libraries

February 11th, 2021 by

The short paper can be found here.

Owicki-Gries Reasoning for C11 RAR

March 7th, 2020 by

The paper can be download from here.

The artifact for the paper can be downloaded from here.

A short video on this work:

The full presentation in ECOOP 2020 can be found here:

SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B

October 7th, 2019 by

The paper can be downloaded from here.

The code generator can be found here.

Towards deductive verification of C11 programs with Event-B and ProB

July 30th, 2019 by

The paper can be found here.

Transforming Event-B models to Dafny contracts

February 1st, 2015 by

From Event-B models to Dafny code contracts

January 1st, 2015 by