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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

15:30 - 17:00: Session ThreeFTfJP at Epernay
15:30 - 16:00
Full-paper
Towards Deductive Verification of C11 Programs with Event-B and ProB
FTfJP
Sadegh DalvandiUniversity of Surrey, Brijesh DongolUniversity of Surrey
16:00 - 16:30
Full-paper
Specifying I/O using Abstract Nested Hoare Triples in Separation Logic
FTfJP
Willem PenninckxKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Bart JacobsKU Leuven
16:30 - 16:45
Short-paper
Analysis of MiniJava Programs via Translation to ML
FTfJP
Martin LesterUniversity of Reading
16:45 - 17:00
Short-paper
Translating Classes to First-Order Logic: An Example
FTfJP