Towards deductive verification of C11 programs with Event-B and ProB
Towards deductive verification of C11 programs with Event-B and ProB
复制标题
使用 Event-B 和 ProB 进行 C11 程序的演绎验证
DOI：
10.1145/3340672.3341117
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Dalvandi M
中科院分区：
文献类型：
--
作者：
Dalvandi M
本文介绍了一种在Event-B框架下对弱内存C11程序进行建模和验证的技术。我们建立在最近开发的操作语义的RAR片段的C11，我们使用作为一个顶级的抽象。在我们的技术中，一个具体的C11程序可以通过细化这个抽象模型的语义建模。程序结构和个人的操作，然后介绍了改进的机器，可以检查和验证使用现有的事件B证明和模型检查。本文还讨论了如何使用ProB模型检查器来验证C11程序的Event-B模型。我们将我们的技术应用于Peterson算法的C11实现，在那里我们发现用于消除互斥的标准不变量是不适当的。因此，我们提出并验证了新的不变量，必要的特征相互排斥在一个弱的记忆设置。
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.
登录
查看更多内容
DOI：
10.1145/3293883.3295702
发表时间：
2018-11
期刊：
Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming
影响因子：
--
作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick
通讯作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick
彻底修改 C11 和 OpenCL 中的 SC 原子
DOI：
10.1145/2837614.2837637
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M
无名稿号（将由编辑插入） 通过对称标记对 B 和 Z 模型进行高效近似验证
DOI：
--
发表时间：
--
期刊：
影响因子：
--
作者：
A. Lanot;A. Boyer;T. Lobbedez;C. Béchade
通讯作者：
C. Béchade
影响因子：
1.8
作者：
Kokologiannakis, Michalis;Lahav, Ori;Vafeiadis, Viktor
通讯作者：
Vafeiadis, Viktor
通过Event-B模型的逐步调度推导并发程序
影响因子：
1
作者：
Pontus Boström;Fredrik Degerlund;K. Sere;M. Waldén
通讯作者：
M. Waldén