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...
Main Authors: | D. V. Efremov, M. U. Mandrykin |
---|---|
Format: | Article |
Language: | English |
Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
Series: | Труды Института системного программирования РАН |
Subjects: | |
Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/418 |
Similar Items
Similar Items
-
Component-based verification of operating systems
by: V. V. Kuliamin, et al.
Published: (2019-02-01) -
Static Verification Tools for C Programs and Linux Device Drivers: A Survey
by: M. U. Mandrykin, et al.
Published: (2018-10-01) -
Applying High-Level Function Loop Invariants for Machine Code Deductive Verification
by: Pavel Andreevitch Putro
Published: (2019-09-01) -
Combining ACSL Specifications and Machine Code
by: P. A. Putro
Published: (2018-10-01) -
Linux Driver Verification
by: D. Beyer, et al.
Published: (2018-10-01)