Sevigator: Network Confinement of Malware Applications and Untrusted Operating Systems. - Denis Efremov 001; Nikolay V. Pakulin (SECRYPT, 2012)

Deductive Verification of Unmodified Linux Kernel Library Functions. - Denis Efremov 001; Mikhail U. Mandrykin; Alexey V. Khoroshilov (ISoLA (2), 2018)

Lemma Functions for Frama-C: C Programs as Proofs. - Grigoriy Volkov; Mikhail U. Mandrykin; Denis Efremov 001 (CoRR, 2018)

Runtime Verification of Linux Kernel Security Module. - Denis Efremov 001; Ilya V. Shchepetkov (FM Workshops (2), 2019)

Runtime Verification of Operating Systems Based on Abstract Models. - Denis Efremov 001; Viktoria V. Kopach; Eugene Kornykhin; Victor V. Kuliamin; Alexander K. Petrenko; Alexey V. Khoroshilov; Ilya V. Shchepetkov (Program. Comput. Softw., 2023)