KVEST: Automated Generation of Test Suites from Formal Specifications. - Igor B. Burdonov; Alexander S. Kossatchev; Alexander K. Petrenko; Dmitri Galter (World Congress on Formal Methods, 1999)

Java Specification Extension for Automated Test Development. - Igor B. Bourdonov; Alexey V. Demakov; Andrew A. Jarov; Alexander S. Kossatchev; Victor V. Kuliamin; Alexander K. Petrenko; Sergey V. Zelenov (Ershov Memorial Conference, 2001)

UniTesK Test Suite Architecture. - Igor B. Bourdonov; Alexander S. Kossatchev; Victor V. Kuliamin; Alexander K. Petrenko (FME, 2002)

Using ASM Specifications for Compiler Testing. - Alexey Ya. Kalinov; Alexander S. Kossatchev; Alexander K. Petrenko; Mikhail Posypkin; Vladimir Shishkov (Abstract State Machines, 2003)

Integration of Functional and Timed Testing of Real-Time and Concurrent Systems. - Victor V. Kuliamin; Alexander K. Petrenko; Nick V. Pakoulin; Alexander S. Kossatchev; Igor B. Bourdonov (Ershov Memorial Conference, 2003)

Coverage-driven Automated Compiler Test Suite Generation. - Alexey Ya. Kalinov; Alexander S. Kossatchev; Alexander K. Petrenko; Mikhail Posypkin; Vladimir Shishkov (LDTA@ETAPS, 2003)

The UniTesK Approach to Designing Test Suites. - Victor V. Kuliamin; Alexander K. Petrenko; Alexander S. Kossatchev; Igor B. Burdonov (Program. Comput. Softw., 2003)

Verification, Validation, and Testing of Software: Special Issue of the Programmirovanie Journal. - Alexander K. Petrenko (Program. Comput. Softw., 2003)

Test Generation for Compilers and Other Formal Text Processors. - Sergey V. Zelenov; Sophia A. Zelenova; Alexander S. Kossatchev; Alexander K. Petrenko (Program. Comput. Softw., 2003)

Preface. - Yuri Gurevich; Alexander K. Petrenko; Alexander S. Kossatchev (MBT, 2004)

Practical Approach to Specification and Conformance Testing of Distributed Network Applications. - Victor V. Kuliamin; Nick V. Pakoulin; Alexander K. Petrenko (ISAS, 2005)

Formal Methods in Industrial Software Standards Enforcement. - Alexey Grinevich; Alexey V. Khoroshilov; Victor V. Kuliamin; Denis Markovtsev; Alexander K. Petrenko; Vladimir V. Rubanov (Ershov Memorial Conference, 2006)

Automatic Test Generation for Model-Based Code Generators. - Sergey V. Zelenov; Denis V. Silakov; Alexander K. Petrenko; Mirko Conrad; Ines Fey (ISoLA, 2006)

The use of contract specifications for representing requirements and for functional testing of hardware models. - V. P. Ivannikov; Alexander S. Kamkin; Alexander S. Kossatchev; Victor V. Kuliamin; Alexander K. Petrenko (Program. Comput. Softw., 2007)

Formal Methods and Innovation Economy: Facing New Challenges. - Alexander K. Petrenko; Olga L. Petrenko (SEFM, 2008)

From the editors of the special issue. - V. A. Nepomnyashchii; Alexander K. Petrenko (Program. Comput. Softw., 2008)

Establishing Linux Driver Verification Process. - Alexey V. Khoroshilov; Vadim S. Mutilin; Alexander K. Petrenko; Vladimir Zakharov (Ershov Memorial Conference, 2009)

Preface. - Bernd Finkbeiner; Yuri Gurevich; Alexander K. Petrenko (MBT@ETAPS, 2009)

Certification of open-source software: A role for formal methods? - Luís Soares Barbosa; Antonio Cerone; Alexander K. Petrenko; Siraj A. Shaikh (Comput. Syst. Sci. Eng., 2010)

Integrating AADL-Based Tool Chain into Existing Industrial Processes. - Alexey V. Khoroshilov; Igor Koverninskiy; Alexander K. Petrenko; Alexander Ugnenko (ICECCS, 2011)

Linux Driver Verification - (Position Paper). - Dirk Beyer 001; Alexander K. Petrenko (ISoLA (2), 2012)

UniTESK: Component Model Based Testing. - Alexander K. Petrenko; Victor V. Kuliamin; Andrey Maksimov (ICTERI, 2013)

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)

Evolution of the UniTESK test development technology. - Victor V. Kuliamin; Alexander K. Petrenko (Program. Comput. Softw., 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)

Preface. - Christophe Gaston; Pascale Le Gall; Alexander K. Petrenko (USE@FM, 2015)

Configurable toolset for static verification of operating systems kernel modules. - Ilja S. Zakharov; Mikhail U. Mandrykin; Vadim S. Mutilin; Evgeny Novikov; Alexander K. Petrenko; Alexey V. Khoroshilov (Program. Comput. Softw., 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)

On Representation of Simulation Time in Functional Programming Style. - Denis V. Buzdalov; Alexander K. Petrenko; Alexey V. Khoroshilov (Program. Comput. Softw., 2019)

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)

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)