This article is cited in 2 papers

Formal verification of Linux kernel library functions

D. V. Efremov^a, M. U. Mandrykin<sup>b

a</sup> NRU Higher School of Economics
^b Ivannikov Institute for System Programming of the Russian Academy of Sciences

Abstract: 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.

Keywords: static analysis, formal verification, deductive verification, standard library.

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

Bibliographic databases:

•