Category:

Our paper “Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL” has been accepted for publication in the Journal of Automated Reasoning

September 28th, 2021 by

Our paper is accepted for publication in the Journal of Automated Reasoning. This paper takes our work on verification of C11 weak memory programs further by showing Nipkow and Nieto’s encoding of Owicki-Gries in the Isabelle theorem prover can be extended to handle C11-style weak memory models in a straightforward manner. We exemplify our techniques over several litmus tests from the literature and a non-trivial example: Peterson’s algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.

A preprint of this work can be found here.

Our poster accepted to PPOPP2021!

February 24th, 2021 by

Our poster “verification of abstract libraries blah blah” was accepted to PPoPP2021. I will present the poster next month.

The preprint of the paper can be found here. The poster can be found here.

Our paper “Owicki-Gries Reasoning for C11 RAR” was accepted to ECOOP 2020

April 9th, 2020 by

Our paper “Owicki-Gries Reasoning for C11 RAR” was accepted to ECOOP 2020.

Our paper “Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B” has been accepted to the International Journal on Software Tools for Technology Transfer

September 18th, 2019 by

Our paper “Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B” has been accepted to the International Journal on Software Tools for Technology Transfer

Our paper “Verifying Cross-layer Interactions through Formal Model-based Assertion Generation” has been accepted to IEEE Embedded Systems Letters.

September 16th, 2019 by

Our paper “Verifying Cross-layer Interactions through Formal Model-based Assertion Generation” has been accepted to IEEE Embedded Systems Letters.