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.
\Bibitem{EfrMan17}
\by D.~V.~Efremov, M.~U.~Mandrykin
\paper Formal verification of Linux kernel library functions
\jour Proceedings of ISP RAS
\yr 2017
\vol 29
\issue 6
\pages 49--76
\mathnet{http://mi.mathnet.ru/tisp273}
\crossref{https://doi.org/10.15514/ISPRAS-2017-29(6)-3}
\elib{https://elibrary.ru/item.asp?id=32309066}
Linking options:
https://www.mathnet.ru/eng/tisp273
https://www.mathnet.ru/eng/tisp/v29/i6/p49
This publication is cited in the following 2 articles:
A. V. Samonov, G. N. Samonova, “Methodology and tools for development and verification of formal fUML models of requirements and architecture for complex software and hardware systems”, Trudy ISP RAN, 30:5 (2018), 123–146
Evgeny Novikov, Ilja Zakharov, Lecture Notes in Computer Science, 11247, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice, 2018, 230
Citation in format AMSBIB
Contact us: