电邮这篇文章 Towards deductive verification of C programs with shared data
- 作者: Mandrykin M.U.1, Khoroshilov A.V.1,2,3,4
-
隶属关系:
- Institute for System Programming
- Moscow State University
- Moscow Institute of Physics and Technology
- National Research University Higher School of Economics
- 期: 卷 42, 编号 5 (2016)
- 页面: 324-332
- 栏目: Article
- URL: https://journals.rcsi.science/0361-7688/article/view/176454
- DOI: https://doi.org/10.1134/S0361768816050054
- ID: 176454
如何引用文章
开放存取
##reader.subscriptionAccessGranted##
订阅存取
详细
This paper considers the problem of the deductive verification of the Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow applying traditional deductive verification techniques, so we consider how to verify such a code by proving its compliance to a given specification of a certain synchronization discipline. The approach is illustrated by the examples of a spinlock specification and a simplified specification of the read-copy-update (RCU) API.
作者简介
M. Mandrykin
Institute for System Programming
编辑信件的主要联系方式.
Email: mandrykin@ispras.ru
俄罗斯联邦, ul. Solzhenitsyna 25, Moscow, 109004
A. Khoroshilov
Institute for System Programming; Moscow State University; Moscow Institute of Physics and Technology; National Research University Higher School of Economics
Email: mandrykin@ispras.ru
俄罗斯联邦, ul. Solzhenitsyna 25, Moscow, 109004; Moscow, 119991; Institutskii per. 9, Dolgoprudnyi, Moscow oblast, 141700; ul. Myasnitskaya 20, Moscow, 101000
补充文件
