A preprint of the paper can be found here.
Category:
Our paper on “Implementing and Verifying Release-Acquire Transactional Memory in C11” has been accepted to OOPSLA 2022!
September 7th, 2022 by sadeghOur paper on “Unifying Operational Weak Memory Verification: An Axiomatic Approach” has been accepted to ACM Transactions on Computational Logic journal.
May 16th, 2022 by sadeghThe paper can be found here.
I joined Axiomise as a Formal Verification Engineer
May 2nd, 2022 by sadeghI joined Axiomise as a formal verification engineer. Excited to see formal verification being applied to industrial-grade designs.
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 sadeghOur 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 sadeghOur 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 sadeghOur 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 sadeghOur 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 sadeghOur paper “Verifying Cross-layer Interactions through Formal Model-based Assertion Generation” has been accepted to IEEE Embedded Systems Letters.