Отправить статью по E-mail 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
Цитировать
Открытый доступ
Доступ предоставлен
Только для подписчиков
Аннотация
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
Дополнительные файлы
