University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Towards Deductive Verification of C11 Programs with Event-B and ProB

Dalvandi, Mohammadsadegh and Dongol, Brijesh (2019) Towards Deductive Verification of C11 Programs with Event-B and ProB In: 21st Workshop on Formal Techniques for Java-like Programs (FTfJP 2019), 15-19 Jul 2019, Novotel London West, Hammersmith, London, United Kingdom.

[img]
Preview
Text
Towards Deductive Verification of C11 Programs with Event-B and ProB.pdf - Accepted version Manuscript

Download (629kB) | Preview

Abstract

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.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computer Science
Authors :
NameEmailORCID
Dalvandi, Mohammadsadeghm.dalvandi@surrey.ac.uk
Dongol, Brijeshb.dongol@surrey.ac.uk
Date : 2019
Funders : Engineering and Physical Sciences Research Council (EPSRC)
DOI : 10.1145/3340672.3341117
Copyright Disclaimer : © 2019 Association for Computing Machinery.
Uncontrolled Keywords : C11; Verification; Event-B; ProB; Model Checking; Peterson’s Algorithm
Related URLs :
Depositing User : Clive Harris
Date Deposited : 19 Aug 2019 10:35
Last Modified : 19 Aug 2019 10:37
URI: http://epubs.surrey.ac.uk/id/eprint/852432

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800