Category:

Implementing and verifying release-acquire transactional memory in C11

November 2nd, 2022 by

Unifying Operational Weak Memory Verification: An Axiomatic Approach

September 7th, 2022 by

The paper can be found here.

Integrating Owicki–Gries for C11-Style Memory Models into Isabelle/HOL

November 16th, 2021 by

The paper can be downloaded from here.

Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B

June 30th, 2020 by

The paper can be downloaded from here.

Verifying Cross-Layer Interactions Through Formal Model-Based Assertion Generation

November 22nd, 2019 by

The paper can be downloaded from here.

A short vide on this work:

Derivation of algorithmic control structures in Event-B refinement

November 19th, 2017 by

The paper can be downloaded from here.

The fully verified Event-B model of the Schorr-Waite graph marking algorithm can be downloaded from here.