Configurable Toolset for Static Verification of Operating Systems Kernel Modules

An operating system (OS) kernel is a critical software regarding to reliability and efficiency. Quality of a modern OSs kernel is high enough. Another situation is with kernel modules, e.g. device drivers, which due to various reasons have a significantly lower level of quality. One of the most crit...

Full description

Bibliographic Details
Published in:	Труды Института системного программирования РАН
Main Authors:	I. S. Zakharov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. Petrenko, A. V. Khoroshilov
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/789

Similar Items

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)

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

Building Programming Interface Specifications in the Open System of Componentwise Verification of the Linux Kernel
by: E. M. Novikov
Published: (2018-10-01)

Approach to Anti-pattern detection in Service-oriented Software Systems
by: A. S. Yugov
Published: (2018-10-01)

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

Adjustable method with predicate abstraction for detection of race conditions in operating systems
by: P. S. Andrianov, et al.
Published: (2018-10-01)

Evolution of the Linux kernel
by: E. M. Novikov
Published: (2018-10-01)

Lightweight Static Analysis for Data Race Detection in Operating System Kernels
by: P. S. Andrianov, et al.
Published: (2018-10-01)

MicroTESK-Based Test Program Generator for the ARMv8 Architecture
by: A. S. Kamkin, et al.
Published: (2018-10-01)

Validation of state machine specifications
by: A. A. Shalyto
Published: (2024-12-01)

Verifying functional properties of smart contracts using symbolic model-checking
by: E. S. Shishkin
Published: (2018-12-01)

Инвазивный подход к верификации функционально-структурных спецификаций, реализованных в заказных интегральных схемах
by: Dmitry Nagibin, et al.
Published: (2025-04-01)

Testing of Linux File System Drivers
by: A. V. Tsyvarev, et al.
Published: (2018-10-01)

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

A declarative language FlexT for analysis and documenting of binary data formats
by: A. Y. Hmelnov, et al.
Published: (2018-10-01)

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

Поиск недостающих вызовов библиотечных функций с использованием машинного обучения
by: I. A. Yakimov, et al.
Published: (2018-10-01)

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

Combination of static verification methods for checking requirements composition
by: V. O. Mordan
Published: (2018-10-01)

Linux Driver Verification
by: D. Beyer, 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)

Introduction to CEGAR —Counter-Example Guided Abstraction Refinement
by: M. U. Mandrykin, et al.
Published: (2018-10-01)

A Flat Chart Technique for Embedded OS Testing
by: V. V. Nikiforov, et al.
Published: (2018-10-01)

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

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

Принципы разработки пользовательских интерфейсов
by: М. В. Урбанович, et al.
Published: (2023-12-01)

Обзор спецификаций системных параметров для анализа микропроцессорной производительности роевого применения БПЛА
by: Д. И. Ковалев
Published: (2024-08-01)

THE IMPROVEMENT OF PUBLIC PROCUREMENT MANAGEMENT AT GOVERNMENT AGENCIES OF MOSCOW
by: S. Zudenkova, et al.
Published: (2016-02-01)

MONITORING OF INFORMATION SECURITY EVENTS in technogenic objectS
by: D. S. Smoliak, et al.
Published: (2019-06-01)

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

Ontology of the “Software Usability” Domain
by: A. A. Sytnik, et al.
Published: (2018-10-01)

Translation of Nested Petri Nets into Classical Petri Nets for Unfoldings Verification
by: V. O. Ermakova, et al.
Published: (2018-10-01)

ОЦІНКА ЯКОСТІ ЖИТТЯ У ХВОРИХ НА ГЕМОБЛАСТОЗИ З УРАЖЕННЯМ НЕРВОВОЇ СИСТЕМИ
by: O.O. Piddubna, et al.
Published: (2017-03-01)

Technology of heterogeneous logging, analysis and report generation
by: S. G. Groshev.
Published: (2018-10-01)

Static Verification Tools for C Programs and Linux Device Drivers: A Survey
by: M. U. Mandrykin, et al.
Published: (2018-10-01)

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

RESEARCH OF STRUCTURE OF HYPOTHALAMIC NUCLEI OF ANIMALS BY METHODS OF FRACTAL GEOMETRY
by: Sergey L'vovich Molchatsky
Published: (2022-09-01)

Static verification for memory safety of Linux kernel drivers
by: A. A. Vasilyev
Published: (2019-02-01)

Specification-Based Test Program Generation for MIPS64 Memory Management Units
by: A. S. Kamkin, et al.
Published: (2018-10-01)

TLA+ based access control model specification
by: A. V. Kozachok
Published: (2018-12-01)