Configurable Toolset for Static Verification of Operating Systems Kernel Modules

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
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:	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/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)

Deductive Verification of Telecommunication Systems Written in C
by: I. S. Anureev
Published: (2012-01-01)

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

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

Construction and Verification of PLC-programs by LTL-specification
by: E. V. Kuzmin, et al.
Published: (2013-01-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)

DEVELOPMENT OF THE SOFTWARE ARCHITECTURE OF A UNIVERSAL SYS- TEM THERMAL IMAGING DIAGNOSTICS
by: V. V. Shitov, et al.
Published: (2013-07-01)

Construction and Verification of PLC LD-programs by LTL-specification
by: E. V. Kuzmin, et al.
Published: (2013-01-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: Adewale Bukola, et al.
Published: (2018-06-01)

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

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

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

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

DESIGNING LOGICAL AND PHYSICAL MODELS OF A UNIVERSAL SYSTEM THERMAL IMAGING DIAGNOSTICS
by: S. T. Antipov, et al.
Published: (2013-07-01)

Predicate Abstractions Memory Modeling Method with Separation into Disjoint Regions
by: A. R. Volkov, 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)

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

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

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

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

Modeling, Specification and Construction of PLC-programs
by: E. V. Kuzmin, et al.
Published: (2013-01-01)

The strategy of testing of the information governance systems of higher educational institution based on the documents with tagged markup
by: N A Sergeeva
Published: (2012-09-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)

INFORMATIONAL SYSTEM FOR PROGRAM PERFORMANCE ESTIMATION
by: A.V. POBEDYONNY
Published: (2018-08-01)

INFORMATIONAL SYSTEM FOR PROGRAM PERFORMANCE ESTIMATION
by: A.V. POBEDYONNY
Published: (2009-06-01)

On the Methodical Principles of Developing the System of Tasks in the Context of the Activity Approach to Teaching Mathematics
by: I V Nasikan
Published: (2012-06-01)