Mon 15 Jul 2019 15:30 - 16:00 at Epernay - Session Three

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

Mon 15 Jul

15:30 - 17:00: FTfJP 2019 - Session Three at Epernay
FTfJP-2019-papers15:30 - 16:00
Sadegh DalvandiUniversity of Surrey, Brijesh DongolUniversity of Surrey
FTfJP-2019-papers16:00 - 16:30
Willem PenninckxKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Bart JacobsKU Leuven
FTfJP-2019-papers16:30 - 16:45
Martin LesterUniversity of Reading
FTfJP-2019-papers16:45 - 17:00