Towards Deductive Verification of C Programs with Shared Data
Mikhail Usamovich Mandrykin, Alexey Vladimirovich Khoroshilov · Proceedings of the Institute for System Programming of RAS · 2015
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.