Formal Verification of OS Security Model with Alloy and Event-B. - Petr N. Devyanin; Alexey V. Khoroshilov; Victor V. Kuliamin; Alexander K. Petrenko; Ilya V. Shchepetkov (ABZ, 2014)

Using Refinement in Formal Development of OS Security Model. - Petr N. Devyanin; Alexey V. Khoroshilov; Victor V. Kuliamin; Alexander K. Petrenko; Ilya V. Shchepetkov (Ershov Memorial Conference, 2015)

Comparison of specification decomposition methods in Event-B. - Petr N. Devyanin; Victor V. Kulyamin; Alexander K. Petrenko; Alexey V. Khoroshilov; Ilya V. Shchepetkov (Program. Comput. Softw., 2016)

Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System. - Petr N. Devyanin; Alexey V. Khoroshilov; Victor V. Kuliamin; Alexander K. Petrenko; Ilya V. Shchepetkov (Program. Comput. Softw., 2020)