Towards Deductive Verification of C Programs with Shared Data

Труды Института системного программирования РАН

M. U. Mandrykin¹  A. V. Khoroshilov¹ 

[1] ИСП РАН;

关键词: верификация;    параллелизм;    владение;    инварианты;    семантика языка c;   

DOI  :  10.15514/ISPRAS-2015-27(4)-4

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown