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