program verification,
program specification,
program semantics,
automated proving,
ontologies.
Subject:
Program verification, program specification, program semantics.
Main publications:
Nepomnyaschii V. A., Anureev I. S., Mikhailov I. N., Promskii A. V., “Na puti k verifikatsii S programm. Yazyk C-light i ego formalnaya semantika”, Programmirovanie, 2002, № 6, 1–13
Anureev I. S., “Operatsionno-ontologicheskii podkhod k formalnoi spetsifikatsii yazykov programmirovaniya”, Programmirovanie, 2009, № 1, 1–11
Nepomnyaschii V. A., Anureev I. S., Promskii A. V., “Na puti k verifikatsii S programm. Aksiomaticheskaya semantika yazyka C-kernel”, Programmirovanie, 2003, № 6, 5–15
Nepomnyaschii V. A., Anureev I. S., Promskii A. V., Dubranovskii I. V., “Na puti k verifikatsii C# programm: trekhurovnevyi podkhod”, Programmirovanie, 2006, № 4, 4–20
Shilov N. V., Anureev I. S., Bodin E. V., “O generatsii uslovii korrektnosti dlya imperativnykh programm”, Programmirovanie, 2008, № 6, 1–20
I. M. Chernenko, I. S. Anureev, “Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms”, Model. Anal. Inform. Sist., 31:4 (2024), 384–425
2.
N. O. Garanina, S. M. Staroletov, V. E. Zyubin, I. S. Anureev, “Model checking programs in process-oriented IEC 61131-3 Structured Text”, Model. Anal. Inform. Sist., 31:1 (2024), 32–53
I. M. Chernenko, I. S. Anureev, N. O. Garanina, “Requirement patterns in deductive verification of poST programs”, Model. Anal. Inform. Sist., 31:1 (2024), 6–31
N. O. Garanina, I. S. Anureev, V. E. Zyubin, S. M. Staroletov, T. V. Liakh, A. S. Rozov, S. P. Gorlatch, “Temporal logic for programmable logic controllers”, Model. Anal. Inform. Sist., 27:4 (2020), 412–427
2019
5.
N. O. Garanina, I. S. Anureev, O. I. Borovikova, V. E. Zyubin, “Methods for domain specification of verification-oriented process ontology”, Model. Anal. Inform. Sist., 26:4 (2019), 534–549
N. V. Shilov, D. A. Kondratyev, I. S. Anureev, E. V. Bodin, A. V. Promsky, “Platform-independent specification and verification of the standard mathematical square root function”, Model. Anal. Inform. Sist., 25:6 (2018), 637–666
N. O. Garanina, I. S. Anureev, O. I. Borovikova, “Verification oriented process ontology”, Model. Anal. Inform. Sist., 25:6 (2018), 607–622
2013
9.
I. S. Anureev, S. N. Baranov, D. M. Beloglazov, E. V. Bodin, P. D. Drobintsev, A. V. Kolchin, V. P. Kotlyarov, A. A. Letichevskii, O. A. Letychevskyi, V. A. Nepomnyashchii, I. V. Nikiforov, S. V. Potiyenko, L. V. Priima, B. V. Tyutin, “Tools of Integrated Technology for Analysis and Verification of Telecom Application Specs”, Tr. SPIIRAN, 26 (2013), 349–383
I. S. Anureev, “Towards technology of development of operational semantics of computer languages: unified format of labelled transition systems”, Tr. SPIIRAN, 25 (2013), 255–276
2012
11.
I. S. Anureev, “Deductive Verification of Telecommunication Systems Written in C”, Model. Anal. Inform. Sist., 19:6 (2012), 34–44
2011
12.
M. M. Atuchin, I. S. Anureev, “Attribute annotations and their use in C program deductive verification”, Model. Anal. Inform. Sist., 18:4 (2011), 21–33
V. A. Nepomnyashchii, I. S. Anureev, M. M. Atuchin, I. V. Mar'yasov, A. A. Petrov, A. V. Promskii, “C program verification in the multilanguage system spectrum”, Model. Anal. Inform. Sist., 17:4 (2010), 88–100
I. S. Anureev, I. V. Mar'yasov, V. A. Nepomnyashchii, “C-programs verification on basis of mixed axiomatic semantics”, Model. Anal. Inform. Sist., 17:3 (2010), 5–28
Contact us: