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

Deductive Verification of Unmodified Linux Kernel Library Functions. - Denis Efremov; 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 (CoRR, 2018)

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

Driving Envelope Definition and Envelope Protection Using Model Predictive Control. - Denis Efremov; Martin Klauco; Tomás Hanis; Martin Hromcík (ACC, 2020)

Haptic Driver Guidance for Lateral Driving Envelope Protection Using Model Predictive Control. - Denis Efremov; Tomás Hanis; Martin Klauco (IV, 2020)

Driving Envelope: On Vehicle Stability Through Tire Capacities. - Denis Efremov; Martin Klauco; Tomás Hanis (IV, 2022)

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

Vehicle and Wheels Stability Defined Using Driving Envelope Protection Algorithm. - Denis Efremov; Tomás Hanis; Martin Klauco (IEEE Trans. Intell. Transp. Syst., 2024)