Towards Deductive Verification of C Programs with Shared Data
The paper takes a look at the problem of deductive verification of Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow to apply traditional deductive verification techniques, so we consider how to verify such code using proof of its compliance to...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/598 |
| id |
doaj-aceaf64b8b474788bae5a0fb3e7a4c41 |
|---|---|
| record_format |
Article |
| spelling |
doaj-aceaf64b8b474788bae5a0fb3e7a4c412020-11-25T00:49:14Zeng Ivannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-01274496810.15514/ISPRAS-2015-27(4)-4598Towards Deductive Verification of C Programs with Shared DataM. U. Mandrykin0A. V. Khoroshilov1ИСП РАНИСП РАН; МГУ имени М.В. Ломоносова, 2-й учебный корпус, факультет ВМК; Московский физико-технический институт (государственный университет); НИУ ВШЭThe paper takes a look at the problem of deductive verification of Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow to apply traditional deductive verification techniques, so we consider how to verify such code using proof of its compliance to a specification of a synchronization discipline. The approach is demonstrated on examples of spinlock specification and a simplified specification of RCU (Read-copy-update) API.https://ispranproceedings.elpub.ru/jour/article/view/598верификацияпараллелизмвладениеинвариантысемантика языка c |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
M. U. Mandrykin A. V. Khoroshilov |
| spellingShingle |
M. U. Mandrykin A. V. Khoroshilov Towards Deductive Verification of C Programs with Shared Data Труды Института системного программирования РАН верификация параллелизм владение инварианты семантика языка c |
| author_facet |
M. U. Mandrykin A. V. Khoroshilov |
| author_sort |
M. U. Mandrykin |
| title |
Towards Deductive Verification of C Programs with Shared Data |
| title_short |
Towards Deductive Verification of C Programs with Shared Data |
| title_full |
Towards Deductive Verification of C Programs with Shared Data |
| title_fullStr |
Towards Deductive Verification of C Programs with Shared Data |
| title_full_unstemmed |
Towards Deductive Verification of C Programs with Shared Data |
| title_sort |
towards deductive verification of c programs with shared data |
| publisher |
Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| series |
Труды Института системного программирования РАН |
| issn |
2079-8156 2220-6426 |
| publishDate |
2018-10-01 |
| description |
The paper takes a look at the problem of deductive verification of Linux kernel code that is concurrent and accesses shared data. The presence of shared data does not allow to apply traditional deductive verification techniques, so we consider how to verify such code using proof of its compliance to a specification of a synchronization discipline. The approach is demonstrated on examples of spinlock specification and a simplified specification of RCU (Read-copy-update) API. |
| topic |
верификация параллелизм владение инварианты семантика языка c |
| url |
https://ispranproceedings.elpub.ru/jour/article/view/598 |
| work_keys_str_mv |
AT mumandrykin towardsdeductiveverificationofcprogramswithshareddata AT avkhoroshilov towardsdeductiveverificationofcprogramswithshareddata |
| _version_ |
1725252234588979200 |