Conditions for the Algorithmic Completeness of Systems of Operations. - Valery A. Nepomniaschy (IFIP Congress (1), 1971)

Criteria for the algorithmic completeness of the systems of operations. - Valery A. Nepomniaschy (International Sympoisum on Theoretical Programming, 1972)

On Divergence Problems for Program Schemas. - Valery A. Nepomniaschy (MFCS, 1976)

On Divergence and Halting Problems for Monadic Program Schemas. - Valery A. Nepomniaschy (MFCS, 1978)

Zur Vollständigkeit von Befehlssystemen. - Valery A. Nepomniaschy; Lutz Voelkel (J. Inf. Process. Cybern., 1978)

Problem-Oriented Means of Program Specification and Verification in Project SPECTRUM. - Valery A. Nepomniaschy; A. A. Sulimov (DISCO, 1993)

REAL92: A Combined Specification Language for Real-Time Concurrent Systems and Properties. - Valery A. Nepomniaschy; Nikolay V. Shilov 002 (Formal Methods in Programming and Their Applications, 1993)

Problem-Oriented Verification System and its Application to Linear Algebra Programs. - Valery A. Nepomniaschy; A. A. Sulimov (Theor. Comput. Sci., 1993)

Petri Net Modelling of Estelle-specified Communication Protocols. - Valery A. Nepomniaschy; Gennady I. Alekseev; Alexandre V. Bystrov; Tatiana G. Churina; Sergey P. Mylnikov; E. V. Okunishnikova (PaCT, 1995)

Verification of Definite Iteration over Hierarchical Data Structures. - Valery A. Nepomniaschy (FASE, 1999)

Symbolic Verification Method for Definite Iteration over Data Structures. - Valery A. Nepomniaschy (Inf. Process. Lett., 1999)

Verification of Estelle-Specified Communication Protocols Using High-Level Petri Nets. - Valery A. Nepomniaschy; Gennady I. Alekseev; Alexandre V. Bystrov; Sergey P. Mylnikov; E. V. Okunishnikova; P. A. Chubarev; Tatiana G. Churina (Program. Comput. Softw., 2001)

Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems. - Valery A. Nepomniaschy; Nikolay V. Shilov 002; Evgeny V. Bodin; Vitaly E. Kozura (IFM, 2002)

Verification of Distributed Systems Modelled by High-Level Petri Nets. - Vitaly E. Kozura; Valery A. Nepomniaschy; Ruslan M. Novikov (PARELEC, 2002)

Verification of Finite Iterations over Tuples of Data Structures. - Valery A. Nepomniaschy (Program. Comput. Softw., 2002)

Towards Verification of C Programs. C-Light Language and Its Formal Semantics. - Valery A. Nepomniaschy; Igor S. Anureev; I. N. Mikhailov; Alexey V. Promsky (Program. Comput. Softw., 2002)

Verification-Oriented Language C-Light and Its Structural Operational Semantics. - Valery A. Nepomniaschy; Igor S. Anureev; Alexey V. Promsky (Ershov Memorial Conference, 2003)

Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language. - Valery A. Nepomniaschy; Igor S. Anureev; Alexey V. Promsky (Program. Comput. Softw., 2003)

Symbolic method of verification of definite iterations over altered data structures. - Valery A. Nepomniaschy (Program. Comput. Softw., 2005)

Towards verification of C# programs: A three-level approach. - Valery A. Nepomniaschy; Igor S. Anureev; I. V. Dubranovskii; Alexey V. Promsky (Program. Comput. Softw., 2006)

Application of Modified Coloured Petri Nets to Modeling and Verification of SDL Specified Communication Protocols. - Valery A. Nepomniaschy; Gennady I. Alekseev; Victor S. Argirov; Dmitri M. Beloglazov; Alexandre V. Bystrov; Eugene A. Chetvertakov; Tatiana G. Churina; Sergey P. Mylnikov; Ruslan M. Novikov (CSR, 2007)

Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs. - Valery A. Nepomniaschy (Pillars of Computer Science, 2008)

Using Coloured Petri Nets to Model and Verify Telecommunications Systems. - Valery A. Nepomniaschy; Dmitri M. Beloglazov; Tatiana G. Churina; Mikhail Mashukov (CSR, 2008)

Modeling and verification of the SDL-specified communication protocols using high-level Petri nets. - Valery A. Nepomniaschy; Victor S. Argirov; Dmitri M. Beloglazov; Alexandre V. Bystrov; Eugene A. Chetvertakov; Tatiana G. Churina (Program. Comput. Softw., 2008)

A Two-Level Approach for Modeling and Verification of Telecommunication Systems. - Dmitri M. Beloglazov; Valery A. Nepomniaschy (Ershov Memorial Conference, 2009)

C-programs verification based on mixed axiomatic semantics. - Igor S. Anureev; Ilya V. Maryasov; Valery A. Nepomniaschy (Autom. Control. Comput. Sci., 2011)

C program verification in SPECTRUM multilanguage system. - Valery A. Nepomniaschy; Igor S. Anureev; M. M. Atuchin; Ilya V. Maryasov; A. A. Petrov; Alexey V. Promsky (Autom. Control. Comput. Sci., 2011)

Deductive verification of the Sliding Window Protocol. - D. A. Chkliaev; Valery A. Nepomniaschy (Autom. Control. Comput. Sci., 2013)

Automatic C program verification based on mixed axiomatic semantics. - Ilya V. Maryasov; Valery A. Nepomnyaschy; Alexey V. Promsky; Dmitry A. Kondratyev (Autom. Control. Comput. Sci., 2014)

Analysis and verification of message sequence charts of distributed systems with the help of coloured Petri nets. - Sergey A. Chernenok; Valery A. Nepomniaschy (Autom. Control. Comput. Sci., 2015)

The language dynamic-real and its application for verification of SDL-specified distributed systems. - Valery A. Nepomniaschy; Evgeny V. Bodin; S. O. Veretnov (Program. Comput. Softw., 2015)

Application of Colored Petri Nets for Verification of Scenario Control Structures in UCM Notation. - N. V. Vizovitin; Valery A. Nepomniaschy; A. A. Stenenko (Autom. Control. Comput. Sci., 2017)

Towards Automatic Deductive Verification of C Programs over Linear Arrays. - Dmitry A. Kondratyev; Ilya V. Maryasov; Valery A. Nepomniaschy (Ershov Informatics Conference, 2019)

The Automation of C Program Verification by the Symbolic Method of Loop Invariant Elimination. - Dmitry A. Kondratyev; Ilya V. Maryasov; Valery A. Nepomniaschy (Autom. Control. Comput. Sci., 2019)

Automation of C Program Deductive Verification without Using Loop Invariants. - Dmitry A. Kondratyev; Valery A. Nepomniaschy (Program. Comput. Softw., 2022)