Мақаланы 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
Қосымша файлдар
