Results 31 to 40 of about 142 (133)
Formal Verification of Linux Kernel Library Functions
Труды Института системного программирования РАН, 2018 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 ...
D. V. Efremov, M. U. Mandrykin
doaj +1 more source
Using static analysis for finding security vulnerabilities and critical errors in source code
Труды Института системного программирования РАН, 2018 Static analysis is a popular way of finding given patterns in source or binary code (e.g., coding style errors, violations of project guidelines of using specific libraries or language features, critical errors, security vulnerabilities, malicious code).
Arutyun Avetisyan +3 more
doaj
Next generation intermediate representations for binary code analysis
Труды Института системного программирования РАН, 2019 A lot of binary code analysis tools do not work directly with machine instructions, instead relying on an intermediate representation from the binary code.
M. A. Solovev +5 more
doaj +1 more source
Component-based verification of operating systems
Труды Института системного программирования РАН, 2019 The paper presents recent results on the way towards accurate and complete verification of industrial operating systems (OS). We consider here OSes, either of general purpose or actively used in some industrial domain, elaborated and maintained for a ...
V. V. Kuliamin +2 more
doaj +1 more source
Lightweight Static Analysis for Data Race Detection in Operating System Kernels
Труды Института системного программирования РАН, 2018 The paper presents an approach to lightweight static data race detection, called CPALockator. It takes into account the specifics of operating system kernels, such as complex parallelism and kernel specifics synchronization mechanisms.
P. S. Andrianov +2 more
doaj +1 more source
Конденсированные среды и межфазные границыВ основе нестехиометрии тугоплавких соединений с летучим компонентом лежат твердофазные и гетерофазные процессы, а измерения параметров высокотемпературных фазовых превращений часто связаны с ошибками и неточностями.
Инга Григорьевна Васильева
doaj +1 more source
Cognitive modelling of processes of public-private partnership in Ukrainian regions Когнитивное моделирование процессов публично-частного партнерства в регионах Украины [PDF]
Problemi Ekonomiki, 2013 The article presents the authors’ view on application of the cognitive modelling when managing processes of activation of the public-private partnership (PPP) in Ukrainian regions. The authors formed a system of concepts of the public and private sectors
Skladannyy D. M. +1 more
doaj
Combining dynamic symbolic execution, code static analysis and fuzzing
Труды Института системного программирования РАН, 2019 This paper describes a new approach for dynamic code analysis. It combines dynamic symbolic execution and static code analysis with fuzzing to increase efficiency of each component.
A. Yu. Gerasimov +5 more
doaj +1 more source
Inter-procedural buffer overflows detection in C/C++ source code via static analysis
Труды Института системного программирования РАН, 2018 We propose inter-procedural static analysis tool for buffer overflow detection. It is based on previously developed intra-procedural algorithm which uses symbolic execution with state merging.
I. . Dudina
doaj +1 more source
Statically detecting buffer overflows in C/C++
Труды Института системного программирования РАН, 2018 The paper describes a static analysis approach for buffer overflow detection in C/C++ source code. This algorithm is designed to be path-sensitive as it is based on symbolic execution with state merging. For now, it works only with buffers on stack or on
I. . Dudina, V. . Koshelev, A. . Borodin
doaj +1 more source