Email this article Towards deductive verification of C programs with shared data
- Authors: Mandrykin M.U.1, Khoroshilov A.V.1,2,3,4
-
Affiliations:
- Institute for System Programming
- Moscow State University
- Moscow Institute of Physics and Technology
- National Research University Higher School of Economics
- Issue: Vol 42, No 5 (2016)
- Pages: 324-332
- Section: Article
- URL: https://journal-vniispk.ru/0361-7688/article/view/176454
- DOI: https://doi.org/10.1134/S0361768816050054
- ID: 176454
Cite item
Open Access
Access granted
Subscription Access
Abstract
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.
About the authors
M. U. Mandrykin
Institute for System Programming
Author for correspondence.
Email: mandrykin@ispras.ru
Russian Federation, ul. Solzhenitsyna 25, Moscow, 109004
A. V. 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
Russian Federation, ul. Solzhenitsyna 25, Moscow, 109004; Moscow, 119991; Institutskii per. 9, Dolgoprudnyi, Moscow oblast, 141700; ul. Myasnitskaya 20, Moscow, 101000
Supplementary files
