16 / 16
И.В. Рудаков, Р.Е. Гурин
64
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
[14] Vartanov S.P., Gerasimov
A.Yu. Dynamic program analysis for error detection using
goal-seeking input data generation.
Sb. tr. ISP RAN
[Proceedings of ISP RAS], 2014, vol. 26,
iss. 1, pp. 375–394. DOI: 10.15514/ISPRAS-2014-26(1)-15
Available at:
http://www.ispras.ru/en/proceedings/isp_26_2014_1/isp_26_2014_1_375/[15] Julien H., Monniaux D., Moy М. PAGAI: a path sensitive static analyzer. Grenoble-INP,
VERIMAG Grenoble France, 2012. 14 p.
[16] Merz F., Falke S., Sinz С. LLBMC: Bounded model checking of C and C++ Programs us-
ing a compiler IR. Institute for Theoretical Computer Science Karlsruhe Institute of Techno-
logy (KIT). Germany, 2012. 16 p.
Rudakov I.V.
— Cand. Sci. (Eng.), Assoc. Professor, Head of Computer Software and Infor-
mation Technology Department, Bauman Moscow State Technical University (2-ya Bauman-
skaya ul. 5, Moscow, 105005 Russian Federation).
Gurin R.E.
— engineer, Bauman Moscow State Technical University (2-ya Baumanskaya ul. 5,
Moscow, 105005 Russian Federation).
Please cite this article in English as:
Rudakov I.V., Gurin R.E. Synthetic Software Verification Method using SMT-Solvers.
Vestn.
Mosk. Gos. Tekh. Univ. im. N.E. Baumana, Priborostr.
[Herald of the Bauman Moscow State
Tech. Univ., Instrum. Eng.], 2016, no. 4, pp. 49–64. DOI: 10.18698/0236-3933-2016-4-49-64