Разработка и исследование синтетического метода верификации программы с помощью SMT-решателей

И.В. Рудаков, Р.Е. Гурин

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4

Holzmann G., Peled D

. An improvement in formal verification // FORTE 1994 Conference.

1994. P. 197–211.

10.

A partial

order approach to branching time logic model checking / R. Gerth, R. Kuiper,

D. Peled, W. Penczek // Inf. Comput. 1999. Vol. 150. No. 2. P. 132–152.

11.

Partial

order reductions preserving simulations / W. Penczek, M. Szreter, R. Gerth,

R. Kuiper // Proc. of Concurrency, Specification and Programming (CSP’99). Warsaw, 1999.

P. 153–172.

12.

Holzmann G.J

. An analysis of bitstate hashing // Formal methods in system design, 1998.

Vol. 13. No. 3. Р. 287–307.

13.

Holzmann G.J

. The spin model checker: Primer and Reference Manual. Addison-Wesley,

2003. 608 p.

14.

Вартанов С.П., Герасимов А.Ю

. Динамический анализ программ с целью поиска

ошибок и уязвимостей при помощи целенаправленной генерации входных данных //

Сб. трудов ИСП РАН. 2014. Т. 26. Вып. 1. C. 375–394.

DOI: 10.15514/ISPRAS-2014-26(1)-15

URL:

http://www.ispras.ru/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 using

a compiler IR. Institute for Theoretical Computer Science Karlsruhe Institute of Technology

(KIT). Germany, 2012. 16 p.

Рудаков Игорь Владимирович

— канд. техн. наук, доцент, заведующий кафедрой «Про-

граммное обеспечение ЭВМ и информационные технологии» МГТУ им. Н.Э. Баумана

(Российская Федерация, 105005, Москва, 2-я Бауманская ул., д. 5).

Гурин Ростислав Евгеньевич

— инженер МГТУ им. Н.Э. Баумана (Российская Федера-

ция, 105005, Москва, 2-я Бауманская ул., д. 5).

Просьба ссылаться на эту статью следующим образом:

Рудаков И.В., Гурин Р.Е. Разработка и исследование синтетического метода верифика-

ции программы с помощью SMT-решателей // Вестник МГТУ им. Н.Э. Баумана. Сер.

Приборостроение. 2016. № 4. C. 49–64. DOI: 10.18698/0236-3933-2016-4-49-64

SYNTHETIC SOFTWARE VERIFICATION METHOD USING SMT-SOLVERS

I.V. Rudakov

irudakov@yandex.ru

R.E. Gurin

rg.bmstu@gmail.com

Bauman Moscow State Technical University, Moscow, Russian Federation

Abstract

Keywords

Non-deterministic behavior of the software remains a pressing

issue. Software verification aims to detect errors, identify vulner-

abilities and check whether the required features are implement-

ed correctly. Verification methods can be divided into groups:

the empirical (using review), formal (using mathematics for

software verification), static (checking the software implementa-

tion without immediate start), dynamic (checking the software

Verification, code analysis, sta-

tic analysis, dynamic analysis,

interpretation, symbolic execu-

tion, model checking