% Publications of Denis Efremov (biblatex format)
%
% Research Identifiers:
%   ORCID:              0000-0002-9916-056X  https://orcid.org/0000-0002-9916-056X
%   ResearcherID (WoS): E-2461-2014
%   SPIN (elibrary.ru): 9415-5917            https://elibrary.ru/author_profile.asp?spin=9415-5917
%   IRID (ISTINA MSU):  812366041            https://istina.msu.ru/workers/812366041/
%   Google Scholar:     Tn954SsAAAAJ         https://scholar.google.com/citations?user=Tn954SsAAAAJ
%   DBLP:               118/1171             https://dblp.org/pid/118/1171.html
%   Semantic Scholar:   48926307             https://www.semanticscholar.org/author/Denis-Efremov/48926307
%   ResearchGate:       Denis-Efremov-4      https://www.researchgate.net/profile/Denis-Efremov-4
%   GitHub:             evdenis              https://github.com/evdenis
%   YouTube:            evdenis

% ============================================================================
% 2025
% ============================================================================

@article{efremov_hardening_overview_2025,
    author = {Efremov, D. V. and Petrenko, A. K. and Pozin, B. A. and Semenov, V. A.},
    title = {Overview of Hardening Mechanisms in Operating Systems and User Applications},
    origtitle = {Обзор механизмов усиления защищенности операционных систем и пользовательских приложений},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2025},
    volume = {37},
    number = {3},
    pages = {325--354},
    doi = {10.15514/ISPRAS-2025-37(3)-23},
    issn = {2079-8156},
    eissn = {2220-6426},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1954},
    langid = {russian},
    abstract = {This paper presents a systematic review of hardening mechanisms for operating systems and user applications. Various types of protection mechanisms are discussed, including memory protection mechanisms, hardware stack protection, dynamic memory protection, address space randomization, control flow protection, and system integrity protection. The principles of these mechanisms, their effectiveness, and their impact on system performance are analyzed in detail. Special attention is given to the implementation of protective mechanisms in modern operating systems, particularly in the Linux kernel.},
    keywords = {hardening, operating systems, memory protection, ASLR, control flow integrity, Linux kernel}
}

@article{petrenko_rv_methods_isp_2025,
    author = {Petrenko, A. K. and Devyanin, P. N. and Efremov, D. V. and Karnov, A. A. and Kornykhin, E. V. and Kuliamin, V. V. and Khoroshilov, A. V.},
    title = {Methods of Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models},
    origtitle = {Методы динамической верификации промышленных средств защиты информации на основе формальных моделей управления доступом},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2025},
    volume = {37},
    number = {3},
    pages = {277--290},
    doi = {10.15514/ISPRAS-2025-37(3)-19},
    issn = {2079-8156},
    eissn = {2220-6426},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1949},
    langid = {russian},
    related = {petrenko_rv_methods_pps_2025},
    relatedtype = {relatedto},
    abstract = {The article addresses runtime verification methods for security protection mechanisms in software systems. It presents a technology combining formal testing techniques with formal access control models and functional specifications, designed for practical industrial application. The approach is illustrated through the new GOST R 59453.4-2025 standard on verifying information security tools implementing access control policies.},
    keywords = {runtime verification, access control, formal methods, security, GOST},
    x-et-al = {3}
}

@article{petrenko_rv_methods_pps_2025,
    author = {Petrenko, A. K. and Efremov, D. V. and Kornykhin, E. V. and Kuliamin, V. V. and Semenov, V. A.},
    title = {Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models},
    origtitle = {Динамическая верификация промышленных средств защиты информации на основе формальных моделей управления доступом},
    journaltitle = {Software \& Systems},
    date = {2025},
    volume = {38},
    number = {2},
    pages = {374--380},
    doi = {10.15827/0236-235X.150.374-380},
    issn = {0236-235X},
    eissn = {2311-2735},
    url = {https://cyberleninka.ru/article/n/dinamicheskaya-verifikatsiya-promyshlennyh-sredstv-zaschity-informatsii-na-osnove-formalnyh-modeley-upravleniya-dostupom},
    langid = {russian},
    related = {petrenko_rv_methods_isp_2025},
    relatedtype = {relatedto},
    abstract = {The work addresses verification methodology for information security mechanisms against formal security models. The authors propose using runtime verification to compare execution traces between an implemented security system and its formal model.},
    keywords = {runtime verification, formal specifications, model-based testing, secure operating systems, secure-by-design}
}

% ============================================================================
% 2023
% ============================================================================

@article{efremov_rv_pcs_2023,
    author = {Efremov, D. V. and Kopach, V. V. and Kornykhin, E. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Runtime Verification of Operating Systems Based on Abstract Models},
    journaltitle = {Programming and Computer Software},
    date = {2023},
    volume = {49},
    number = {7},
    pages = {559--565},
    doi = {10.1134/S0361768823070034},
    issn = {0361-7688},
    eissn = {1608-3261},
    publisher = {Pleiades Publishing},
    langid = {english},
    related = {efremov_rv_isp_2021},
    relatedtype = {translationof},
    abstract = {High complexity of a modern operating system (OS) requires to use complex models and high-level specification languages to describe even separated aspects of OS functionality, e.g., security functions. Use of such models in conformance verification of modeled OS needs to establish rather complex relation between elements of OS implementation and elements of the model. In this paper we present a method to establish and support such a relation, which can be effectively used in testing and runtime verification/monitoring of OS. The method described was used successfully in testing and monitoring of Linux OS core components on conformance to Event-B models.},
    keywords = {runtime verification, Linux kernel, LSM, IMA/EVM, Event-B, ProB},
    x-pdf = {efremov_rv_pcs_2023_draft.pdf}
}

% ============================================================================
% 2021
% ============================================================================

@article{efremov_rv_isp_2021,
    author = {Efremov, D. V. and Kopach, V. V. and Kornykhin, E. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Runtime Verification of Operating Systems Based on Abstract Models},
    origtitle = {Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2021},
    volume = {33},
    number = {6},
    pages = {15--26},
    doi = {10.15514/ISPRAS-2021-33(6)-2},
    issn = {2079-8156},
    eissn = {2220-6426},
    publisher = {Institute for System Programming of the Russian Academy of Sciences},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1469},
    langid = {russian},
    related = {efremov_rv_pcs_2023},
    relatedtype = {translatedas},
    abstract = {High complexity of a modern operating system (OS) requires to use complex models and high-level specification languages to describe even separated aspects of OS functionality, e.g., security functions. Use of such models in conformance verification of modeled OS needs to establish rather complex relation between elements of OS implementation and elements of the model. In this paper we present a method to establish and support such a relation, which can be effectively used in testing and runtime verification/monitoring of OS. The method described was used successfully in testing and monitoring of Linux OS core components on conformance to Event-B models.},
    keywords = {runtime verification, Linux Kernel, LSM, IMA/EVM, Event-B, ProB}
}

% ============================================================================
% 2020
% ============================================================================

@article{petrenko_multilevel_specs_2020,
    author = {Petrenko, A. K. and Efremov, D. V. and Kornykhin, E. V. and Kuliamin, V. V. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Monitoring and Testing Based on Multi-Level Program Specifications},
    origtitle = {Мониторинг и тестирование на основе многоуровневых спецификаций программ},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2020},
    volume = {32},
    number = {6},
    pages = {7--18},
    doi = {10.15514/ISPRAS-2020-32(6)-1},
    issn = {2079-8156},
    eissn = {2220-6426},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/1357},
    langid = {russian},
    abstract = {The paper addresses building multi-level specifications for formal verification. Testing using formal models should employ the same specifications used in formal verification. The authors examine various development methods, integration possibilities, and constraints for test and monitoring systems.},
    keywords = {testing, monitoring, formal specifications, verification}
}

@inproceedings{efremov_rv_lsm_fm2019,
    author = {Efremov, Denis and Shchepetkov, Ilya},
    editor = {Sekerinski, Emil and Moreira, Nelma and Oliveira, Jos{\'e} N. and Ratiu, Daniel and et al.},
    title = {Runtime Verification of Linux Kernel Security Module},
    booktitle = {Formal Methods. FM 2019 International Workshops},
    series = {Lecture Notes in Computer Science},
    volume = {12233},
    date = {2020},
    publisher = {Springer International Publishing},
    location = {Cham},
    pages = {185--199},
    doi = {10.1007/978-3-030-54997-8_12},
    isbn = {978-3-030-54997-8},
    printisbn = {978-3-030-54996-1},
    issn = {0302-9743},
    eissn = {1611-3349},
    url = {https://link.springer.com/chapter/10.1007/978-3-030-54997-8_12},
    langid = {english},
    eprint = {2001.01442},
    eprinttype = {arxiv},
    eprintclass = {cs.SE},
    abstract = {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 sensitive, confidential or simply private data. It is crucial to establish and prove its security properties. This work-in-progress paper presents a method to verify the Linux kernel for conformance with an abstract security policy model written in the Event-B specification language. The method is based on system call tracing and aims at checking that the results of system call execution do not lead to accesses that violate security policy requirements.},
    keywords = {runtime verification, Linux kernel, LSM, Event-B},
    x-venue = {FM 2019 International Workshops}
}

% ============================================================================
% 2019
% ============================================================================

@book{devyanin_security_monograph_2019,
    author = {Devyanin, P. N. and Efremov, D. V. and Kuliamin, V. V. and Petrenko, A. K. and Khoroshilov, A. V. and Shchepetkov, I. V.},
    title = {Modeling and Verification of Access Control Security Policies in Operating Systems},
    origtitle = {Моделирование и верификация политик безопасности управления доступом в операционных системах},
    publisher = {Goryachaya Liniya -- Telekom},
    date = {2019},
    location = {Moscow, Russian Federation},
    pagetotal = {214},
    isbn = {978-5-9912-0787-4},
    langid = {russian},
    url = {http://www.ispras.ru/publications/2018/security_policy_modeling_and_verification/},
    keywords = {access control, security policy, formal verification, operating systems}
}

@report{acsl_by_example_2019,
    author = {Gerlach, Jens and Efremov, Denis and Sikatzki, Tim and others},
    title = {{ACSL by Example}: Towards a Formally Verified Standard Library},
    type = {Technical Report},
    institution = {Fraunhofer {FOKUS}},
    date = {2019-06},
    version = {19.0.0},
    url = {https://github.com/fraunhoferfokus/acsl-by-example/raw/master/ACSL-by-Example.pdf},
    langid = {english},
    keywords = {ACSL, Frama-C, formal verification, standard library},
    x-type = {Technical Report},
    x-venue = {Fraunhofer FOKUS},
    x-external-pdf = {https://github.com/fraunhoferfokus/acsl-by-example/raw/master/ACSL-by-Example.pdf}
}

% ============================================================================
% 2018
% ============================================================================

@inproceedings{efremov_verker_isola_2018,
    author = {Efremov, Denis and Mandrykin, Mikhail and Khoroshilov, Alexey},
    editor = {Margaria, Tiziana and Steffen, Bernhard},
    title = {Deductive Verification of Unmodified Linux Kernel Library Functions},
    booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. Verification},
    series = {Lecture Notes in Computer Science},
    volume = {11245},
    date = {2018},
    publisher = {Springer International Publishing},
    location = {Cham},
    pages = {216--234},
    doi = {10.1007/978-3-030-03421-4_15},
    isbn = {978-3-030-03421-4},
    printisbn = {978-3-030-03420-7},
    issn = {0302-9743},
    eissn = {1611-3349},
    url = {https://link.springer.com/chapter/10.1007/978-3-030-03421-4_15},
    eprint = {1809.00626},
    eprinttype = {arxiv},
    langid = {english},
    related = {efremov_verker_ispras_2017},
    relatedtype = {extends},
    abstract = {This paper presents results from the development and evaluation of a deductive verification benchmark consisting of 26 unmodified Linux kernel library functions implementing conventional memory and string operations. The formal contract of the functions was extracted from their source code and was represented in the form of preconditions and postconditions. The correctness of 23 functions was completely proved using AstraVer toolset, although success for 11 functions was achieved using 2 new specification language constructs. Another 2 functions were proved after a minor modification of their source code, while the final one cannot be completely proved using the existing memory model.},
    keywords = {deductive verification, Linux kernel, Frama-C, ACSL, AstraVer},
    x-venue = {ISoLA 2018}
}

@inproceedings{volkov_lemma_functions_2018,
    author = {Volkov, Grigoriy and Mandrykin, Mikhail and Efremov, Denis},
    title = {Lemma Functions for {Frama-C}: {C} Programs as Proofs},
    booktitle = {Proceedings of the 2018 Ivannikov ISPRAS Open Conference (ISPRAS-2018)},
    date = {2018},
    pages = {31--38},
    doi = {10.1109/ISPRAS.2018.00012},
    isbn = {978-1-7281-1275-6},
    printisbn = {978-1-7281-1276-3},
    publisher = {IEEE},
    url = {https://ieeexplore.ieee.org/document/8675145},
    eprint = {1811.05879},
    eprinttype = {arxiv},
    langid = {english},
    abstract = {The paper presents an auto-active verification technique developed within the Frama-C framework. It details the lemma functions method and presents the corresponding ACSL extension, its implementation in Frama-C, and evaluation on a set of string-manipulating functions from the Linux kernel.},
    keywords = {formal verification, deductive verification, Frama-C, ACSL, auto-active verification, lemma functions, Linux kernel},
    x-venue = {ISPRAS Open 2018}
}

% ============================================================================
% 2017
% ============================================================================

@article{efremov_verker_ispras_2017,
    author = {Efremov, Denis and Mandrykin, Mikhail},
    title = {Formal Verification of Linux Kernel Library Functions},
    origtitle = {Формальная верификация библиотечных функций ядра Linux},
    journaltitle = {Proceedings of the Institute for System Programming of the RAS},
    date = {2017},
    volume = {29},
    number = {6},
    pages = {49--76},
    doi = {10.15514/ISPRAS-2017-29(6)-3},
    issn = {2079-8156},
    eissn = {2220-6426},
    url = {https://ispranproceedings.elpub.ru/jour/article/view/418},
    langid = {russian},
    related = {efremov_verker_isola_2018,verker_github_2017},
    relatedtype = {extendedby,supplementedby},
    keywords = {formal verification, Linux kernel, Frama-C, ACSL}
}

% ============================================================================
% 2015
% ============================================================================

@book{efremov_osdev_book_2015,
    author = {Efremov, D. V. and Komarov, N. Yu. and Khoroshilov, A. V.},
    title = {Construction of the Operating System Kernel},
    origtitle = {Конструирование ядра операционной системы},
    publisher = {Publishing Department of the CMC Faculty of Lomonosov Moscow State University; MAKS Press},
    date = {2015},
    location = {Moscow},
    pagetotal = {160},
    isbn = {978-5-89407-549-5},
    langid = {russian},
    url = {https://www.elibrary.ru/item.asp?id=25670418},
    keywords = {operating systems, kernel, education},
    x-type = {Textbook},
    x-publisher-short = {MSU/MAKS Press}
}

% ============================================================================
% 2014
% ============================================================================

@inproceedings{efremov_verif_tools_2014,
    author = {Efremov, Denis and Komarov, Nikita},
    title = {Tools Support for Linux Kernel Deductive Verification Workflow},
    booktitle = {Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE)},
    date = {2014},
    volume = {8},
    number = {6},
    pages = {39--44},
    doi = {10.15514/SYRCOSE-2014-8-6},
    issn = {2311-7230},
    url = {https://cyberleninka.ru/article/n/tools-support-for-linux-kernel-deductive-verification-workflow},
    location = {Saint Petersburg, Russia},
    langid = {english},
    abstract = {The paper examines formal verification of a Linux kernel security module through deductive methods. The authors describe their chosen toolset (Frama-C, Why, Jessie), the verification workflow, and auxiliary tools they developed. Key challenges addressed include handling C language extensions, managing dependencies with kernel headers, and coordinating specifications development during active code development.},
    keywords = {formal verification, Linux kernel, deductive verification, security modules, Frama-C},
    x-venue = {SYRCoSE 2014}
}

% ============================================================================
% 2012
% ============================================================================

@inproceedings{efremov_sevigator_2012,
    author = {Efremov, Denis and Pakulin, Nikolay},
    title = {Sevigator: Network Confinement of Malware Applications and Untrusted Operating Systems},
    booktitle = {Proceedings of the International Conference on Security and Cryptography (SECRYPT 2012)},
    date = {2012},
    pages = {395--398},
    isbn = {978-989-8565-24-2},
    doi = {10.5220/0004070103950398},
    publisher = {SciTePress},
    location = {Rome, Italy},
    url = {https://www.researchgate.net/publication/233968192_Sevigator_Network_Confinement_of_Malware_Applications_and_Untrusted_Operating_Systems},
    langid = {english},
    abstract = {The paper presents Sevigator -- a toolkit for network confinement where only trusted applications gain access to the local network while other applications and even the OS kernel have no networking at all. Sevigator is based on hardware virtualization support: a custom hypervisor hides network interface card from the OS kernel and delegates network-based system calls of trusted applications to a dedicated service virtual machine.},
    keywords = {virtualization-based security, network access control, hypervisor, virtual machine monitor, malware},
    x-venue = {SECRYPT 2012}
}

% ============================================================================
% 2011
% ============================================================================

@inproceedings{efremov_hypervisor_2011,
    author = {Efremov, Denis},
    title = {Protection of the Applications' Privacy Running Untrusted Operating System},
    origtitle = {Защита приватности приложений в недоверенной операционной системе},
    booktitle = {Proceedings of the Russian Conference on Actual Problems of System and Software Engineering (APSSE)},
    date = {2011},
    langid = {russian},
    keywords = {virtualization, privacy, security},
    x-venue = {APSSE 2011}
}

% ============================================================================
% 2010
% ============================================================================

@inproceedings{efremov_sec_activation_2010,
    author = {Efremov, Denis and Iakovenko, Pavel},
    title = {An Approach to On-the-Fly Activation and Deactivation of Virtualization-Based Security Systems},
    booktitle = {Proceedings of the Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE)},
    date = {2010},
    volume = {4},
    pages = {157--161},
    doi = {10.15514/SYRCOSE-2010-4-31},
    issn = {2311-7230},
    url = {https://cyberleninka.ru/article/n/an-approach-to-on-the-fly-activation-and-deactivation-of-virtualization-based-security-systems},
    location = {Nizhny Novgorod, Russia},
    langid = {english},
    abstract = {The authors present a method for on-the-fly activation and deactivation of hardware virtualization based security systems that protect applications running under untrusted operating systems. The approach addresses resource reservation from the OS for hypervisor and additional virtual machines, while considering threats from malicious startup and shutdown environments.},
    keywords = {VMM, hypervisor, virtual machine monitor, virtualization, secure activation},
    x-venue = {SYRCoSE 2010}
}

% ============================================================================
% Software Registrations (FIPS - Rospatent)
% ============================================================================

@misc{cvehound_fips_2021,
    author = {Efremov, Denis},
    title = {{CVEhound}},
    date = {2021-08-17},
    howpublished = {State Registration of Computer Program, Russian Federation},
    note = {Registration No. RU 2021663474},
    url = {https://new.fips.ru/registers-doc-view/fips_servlet?DB=EVM&DocNumber=2021663474&TypeFile=html},
    langid = {russian},
    organization = {Institute for System Programming of the Russian Academy of Sciences},
    related = {cvehound_github_2021},
    relatedtype = {supplementedby},
    keywords = {CVE, Linux kernel, security, Coccinelle, software registration}
}

@misc{eventb_syscall_replay_fips_2020,
    author = {Efremov, Denis},
    title = {System Call Replay on Event-B Models},
    origtitle = {Программа воспроизведения системных вызовов операционной системы на Event-B модели},
    date = {2020-10-01},
    howpublished = {State Registration of Computer Program, Russian Federation},
    note = {Registration No. RU 2020661855},
    url = {https://new.fips.ru/registers-doc-view/fips_servlet?DB=EVM&DocNumber=2020661855&TypeFile=html},
    langid = {russian},
    organization = {Institute for System Programming of the Russian Academy of Sciences},
    related = {efremov_rv_lsm_fm2019,efremov_rv_isp_2021},
    relatedtype = {supplementto,supplementto},
    keywords = {Event-B, runtime verification, system calls, software registration}
}

@misc{c_code_transform_fips_2015,
    author = {Efremov, Denis and Khoroshilov, Alexey},
    title = {C Source Code Transformation for Subsequent Verification},
    origtitle = {Программа преобразования структуры исходного кода на языке С для его последующей верификации},
    date = {2015-07-27},
    howpublished = {State Registration of Computer Program, Russian Federation},
    note = {Registration No. RU 2015617942},
    url = {https://new.fips.ru/registers-doc-view/fips_servlet?DB=EVM&DocNumber=2015617942&TypeFile=html},
    langid = {russian},
    organization = {Institute for System Programming of the Russian Academy of Sciences},
    keywords = {C language, source code transformation, verification, software registration}
}

% ============================================================================
% Open Source Projects (GitHub)
% ============================================================================

@software{cvehound_github_2021,
    author = {Efremov, Denis},
    title = {{CVEhound}: Audit Kernel Sources for Missing CVE Fixes},
    date = {2021},
    url = {https://github.com/evdenis/cvehound},
    note = {Open source tool for scanning Linux kernel sources for known CVEs using Coccinelle semantic patches},
    langid = {english},
    related = {cvehound_fips_2021},
    relatedtype = {supplementto},
    keywords = {CVE, Linux kernel, security, Coccinelle}
}

@software{verker_github_2017,
    author = {Efremov, Denis},
    title = {{VerKer}: Formal Verification of Linux Kernel Library Functions},
    date = {2017},
    url = {https://github.com/evdenis/verker},
    note = {Benchmark and tools for deductive verification of Linux kernel library functions using Frama-C/ACSL},
    langid = {english},
    related = {efremov_verker_ispras_2017,efremov_verker_isola_2018},
    relatedtype = {supplementto,supplementto},
    keywords = {formal verification, Linux kernel, Frama-C, ACSL}
}

@software{spec_utils_github_2017,
    author = {Efremov, Denis},
    title = {{Spec-Utils}: Tools for Writing ACSL Specifications for Linux Kernel},
    date = {2017},
    url = {https://github.com/evdenis/spec-utils},
    note = {Perl-based tools for extracting and preparing Linux kernel code for ACSL specification development},
    langid = {english},
    related = {efremov_verker_ispras_2017,efremov_verker_isola_2018},
    relatedtype = {supplementto,supplementto},
    keywords = {ACSL, Linux kernel, specifications, tools}
}

% ============================================================================
% Presentations & Talks
% ============================================================================

% Linux Security Summit 2021
@misc{talk_cvehound_lss_2021,
    author = {Efremov, Denis},
    title = {{CVEhound}: Audit Kernel Sources for Missing {CVE} Fixes},
    date = {2021},
    howpublished = {Linux Security Summit 2021 (LSS2021)},
    note = {Conference talk},
    url = {https://www.youtube.com/watch?v=tZMv0EzjPh0},
    urlslides = {https://speakerdeck.com/efremov/cvehound-audit-kernel-sources-for-missing-cve-fixes},
    langid = {english},
    related = {cvehound_github_2021},
    relatedtype = {supplementto},
    keywords = {CVE, Linux kernel, security, Coccinelle, presentation}
}

% ZeroNights 2021
@misc{talk_cvehound_zeronights_2021,
    author = {Efremov, Denis},
    title = {{CVEhound}: проверка исходников {Linux} на известные {CVE}},
    date = {2021},
    howpublished = {ZeroNights 2021},
    note = {Conference talk},
    url = {https://www.youtube.com/watch?v=-QwLkpYzQIk},
    urlslides = {https://speakerdeck.com/efremov/cvehound-audit-kernel-sources-for-missing-cve-fixes},
    langid = {russian},
    related = {cvehound_github_2021},
    relatedtype = {supplementto},
    keywords = {CVE, Linux kernel, security, Coccinelle, presentation}
}

% OSSDEVCONF-2021
@misc{talk_linux_testing_ossdevconf_2021,
    author = {Efremov, Denis},
    title = {Инструменты тестирования ядра {Linux}},
    date = {2021-06-17},
    howpublished = {OSSDEVCONF-2021},
    note = {Conference presentation},
    url = {https://www.youtube.com/watch?v=wsLAJ9tyJYE},
    urlslides = {https://speakerdeck.com/efremov/instrumienty-tiestirovaniia-iadra-linux},
    langid = {russian},
    keywords = {Linux kernel, testing, KUnit, kselftest, LTP, presentation}
}

% ISoLA 2018 presentation
@misc{talk_verker_isola_2018,
    author = {Efremov, Denis and Mandrykin, Mikhail and Khoroshilov, Alexey},
    title = {Deductive Verification of Unmodified {Linux} Kernel Library Functions},
    date = {2018-11},
    howpublished = {ISoLA 2018, Limassol, Cyprus},
    note = {Conference presentation},
    url = {https://www.slideshare.net/slideshow/deductive-verification-of-unmodified-linux-kernel-library-functions/129692925},
    langid = {english},
    related = {efremov_verker_isola_2018},
    relatedtype = {supplementto},
    keywords = {deductive verification, Linux kernel, Frama-C, ACSL, presentation}
}

% PHDays VII (2017)
@misc{talk_formal_verif_c_phdays_2017,
    author = {Efremov, Denis},
    title = {Формальная верификация кода на языке {C}},
    date = {2017},
    howpublished = {Positive Hack Days VII (PHDays VII)},
    note = {Conference talk},
    url = {https://www.youtube.com/watch?v=ZQlm0vZ_bSI},
    urlslides = {https://www.slideshare.net/slideshow/efremov-verification-animation-final/77881985},
    langid = {russian},
    keywords = {formal verification, C language, deductive verification, presentation}
}

% PHDays X (2021)
@misc{talk_formal_verif_os_phdays_2021,
    author = {Efremov, Denis},
    title = {Формальная верификация ядер операционных систем},
    date = {2021},
    howpublished = {Positive Hack Days X (PHDays X)},
    note = {Conference talk},
    url = {https://www.youtube.com/watch?v=qjwqGu07HIU},
    urlslides = {https://speakerdeck.com/efremov/formal-verification-of-operating-system-kernels},
    langid = {russian},
    keywords = {formal verification, operating systems, Linux kernel, presentation}
}