Proceedings of ISP RAS

Formal Verification of Linux Kernel Library Functions

Efremov D.V. (HSE, Moscow, Russia)
Mandrykin M.U. (ISP RAS, Moscow, Russia)


The paper presents result of a study on deductive verification of 26 Linux kernel library functions with AstraVer toolset. The code includes primarily string-manipulating functions and is verified against contract specifications formalizing its functional correctness properties. The paper presents a brief review of the related earlier studies, discusses their results and indicates both the previous issues that were successfully solved in this study and the ones that remain and still prevent successful verification. The paper also presents several specification practices that were applied in the study, including some common specification patterns. The authors have successfully and fully proved functional correctness of 25 functions. The paper includes results of benchmarking 5 state-of-the-art SMT solvers on the resulting verification conditions.


static analysis; formal verification; deductive verification; standard library


Proceedings of the Institute for System Programming, vol. 29, issue 6, 2017, pp. 49-76.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(6)-3

Full text of the paper in pdf (in Russian) Back to the contents of the volume