3 papers
cs.SE2020
Runtime Verification of Linux Kernel Security Module
Denis Efremov, Ilya Shchepetkov
The Linux kernel is one of the most important Free/Libre Open Source Software (FLOSS) projects. It is installed on billions of devices all over the world, which process various sen…
cs.SE2018
Lemma Functions for Frama-C: C Programs as Proofs
Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov
This paper describes the development of an auto-active verification technique in the Frama-C framework. We outline the lemma functions method and present the corresponding ACSL ext…
cs.SE2018
Deductive Verification of Unmodified Linux Kernel Library Functions
Denis Efremov, Mikhail Mandrykin, Alexey Khoroshilov
This paper presents results from the development and evaluation of a deductive verification benchmark consisting of 26 unmodified Linux kernel library functions implementing conven…