Mohammadsadegh Dalvandi

Dr Sadegh Dalvandi

My publications


Dalvandi Mohammadsadegh, Dongol Brijesh (2019) Towards Deductive Verification of C11 Programs with Event-B and ProB, Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019) Association for Computing Machinery (ACM)
This paper introduces a technique for modelling and verifying
weak memory C11 programs in the Event-B framework.
We build on a recently developed operational semantics for
the RAR fragment of C11, which we use as a top-level abstraction.
In our technique, a concrete C11 program can be
modelled by refining this abstract model of the semantics.
Program structures and individual operations are then introduced
in the refined machine and can be checked and
verified using available Event-B provers and model checkers.
The paper also discusses how ProB model checker can be
used to validate the Event-B model of C11 programs. We applied
our technique to the C11 implementation of Peterson?s
algorithm, where we discovered that the standard invariant
used to characterise mutual exclusion is inadaquate. We
therefore propose and verify new invariants necessary for
characterising mutual exclusion in a weak memory setting.