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
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
2020
3.
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
4.
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
8.
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
10.
I. S. Anureev, “Deductive Verification of Telecommunication Systems Written in C”, Model. Anal. Inform. Sist., 19:6 (2012), 34–44
2011
11.
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: