Formal Verification of Linux Kernel Library Functions

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

Full description

Bibliographic Details
Published in:Труды Института системного программирования РАН
Main Authors: D. V. Efremov, M. U. Mandrykin
Format: Article
Language:English
Published: Russian Academy of Sciences, Ivannikov Institute for System Programming 2018-10-01
Subjects:
Online Access:https://ispranproceedings.elpub.ru/jour/article/view/418