Formal Verification of Linux Kernel Library Functions

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

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)

Formal Verification of Three-Valued Digital Waveforms
by: Nina Yu. Kutsak, et al.
Published: (2019-09-01)

Linux Driver Verification
by: D. Beyer, et al.
Published: (2018-10-01)

Designing robust quadcopter software based on a real-time partitioned operating system and formal verification techniques
by: Sergey Mikhailovich Staroletov, et al.
Published: (2019-10-01)

Formal Verification of Programs in Functional Dataflow Parallel Language
by: M. S. Kropacheva, et al.
Published: (2015-03-01)

Formal Verification of Programs in Functional Dataflow Parallel Language
by: M. S. Kropacheva, et al.
Published: (2012-01-01)

Combining ACSL Specifications and Machine Code
by: P. A. Putro
Published: (2018-10-01)

Usability of AutoProof: a case study of software verification
by: Mansur Khazeev, et al.
Published: (2018-10-01)

Linux Driver Verification Architecture
by: V. S. Mutilin, et al.
Published: (2018-10-01)

Verication and synthesis of addition programs under the rules of statement correctness
by: V. I. Shelekhov
Published: (2010-12-01)

A Formal Model and Verification Problems for Software Defined Networks
by: V. A. Zakharov, et al.
Published: (2013-12-01)

A Formal Model and Verification Problems for Software Defined Networks
by: V. A. Zakharov, et al.
Published: (2013-01-01)

Approach to test program development for multilevel verification
by: Pavel Viktorovich Frolov
Published: (2019-09-01)

Attribute Annotations and Their Use in C Program Deductive Verification
by: M. M. Atuchin, et al.
Published: (2011-12-01)

Architecture of the Formally-Verified Distributed Ledger System InnoChain
by: Leonid Al'bertovich Merkin-Janson, et al.
Published: (2020-12-01)

Survey of memory modeling methods in static verification tools
by: M. U. Mandrykin, et al.
Published: (2018-10-01)

Verified program code execution system prototype
by: A. V. Kozachok, et al.
Published: (2018-10-01)

Static verification of operating system monolithic kernels
by: E. M. Novikov
Published: (2018-10-01)

Towards Neural Routing with Verified Bounds on Performance
by: Igor Petrovich Buzhinsky, et al.
Published: (2022-09-01)

Automation of Formal Veriﬁcation of Programs in the Pifagor Language
by: M. S. Ushakova, et al.
Published: (2015-08-01)

Integration Points of Operating System Verification Techniques
by: A. K. Petrenko, et al.
Published: (2018-10-01)

Towards Deductive Verification of C Programs with Shared Data
by: M. U. Mandrykin, et al.
Published: (2018-10-01)

Temporal Logic for Programmable Logic Controllers
by: Natalia Olegovna Garanina, et al.
Published: (2020-12-01)

Linux kernel configuration build for application systems
by: S. V. Kozin
Published: (2019-02-01)

Deductive Verification of the Sliding Window Protocol
by: D. A. Chkliaev, et al.
Published: (2015-03-01)

Deductive Verification of the Sliding Window Protocol
by: D. A. Chkliaev, et al.
Published: (2012-01-01)

Environment Modeling of Linux Operating System Device Drivers
by: I. S. Zakharov, et al.
Published: (2018-10-01)

Immunochromatographic method in the diagnosis of pneumococcal respiratory tract diseases
by: V. V. Nikolenko, et al.
Published: (2014-09-01)

Simulation-based Verification of System-on-Chip Bus Controllers
by: M. M. Chupilko, et al.
Published: (2018-10-01)

Predicate Abstractions Memory Modeling Method with Separation into Disjoint Regions
by: A. R. Volkov, et al.
Published: (2018-10-01)

Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System
by: Dmitry A. Kondratyev
Published: (2021-12-01)

Verification Oriented Process Ontology
by: Natalia O. Garanina, et al.
Published: (2018-12-01)

Tool for Behavioral Analysis of Well-Structured Transition Systems
by: L. V. Dworzanski, et al.
Published: (2018-10-01)

Incremental development of environment model and requirement specifications for subsystems of operating system monolithic kernels
by: I. S. Zakharov, et al.
Published: (2018-10-01)

The refactoring approach used in Klocwork Insight toolkit
by: N. L. Lugovskoy
Published: (2018-10-01)

A Model Checking-Based Method of Functional Test Generation for HDL Descriptions
by: M. S. Lebedev, et al.
Published: (2018-10-01)

Verification and analysis of variable operating systems
by: V. V. Kuliamin, et al.
Published: (2018-10-01)

Test environment for verification of multi-processor memory subsystem unit
by: Dmitry Alexeevitch Lebedev, et al.
Published: (2019-09-01)