15 / 16
Разработка и исследование синтетического метода верификации программы…
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4
63
implementation through direct start), with different levels of
automation. Existing verification methods are flawed as there is
an exponential increase in the number of states (combinatorial
explosion). One way to resolve this problem is to create a syn-
thetic method. We offer a synthetic software verification method
based on SMT — solver that does not require a complex model.
Its algorithm is implemented using SMT-LIB
REFERENCES
[1] Buryakova N.A., Chernov A.V. Classification of partially formal and formal models and
methods for software verification.
Inzhenernyy vestnik Dona
[Electron. sci. journ. Engineering
Journal of Don], 2010, vol. 14, no. 4. Available at:
http://www.ivdon.ru/ru/magazine/archive/n4y2010/259
[2] Vel'der S.E., Shalyto A.A. Verification of simple automate programs on the basis of the
modelchecking method. ModelChecking.
Mat. XV Mezhdunar. nauch.-metodich. konf.
“Vysokie intellektual'nye tekhnologii i innovatsii v obrazovanii i nauke”
[Highly intellectual
technologies and innovations in education and science], 2008, p. 286 (in Russ.).
[3] Holzmann G., Smith M. Software model checking: Extracting verification models from
source code.
Formal methods for protocol engineering and distributed systems
. Kluwer Academ-
ic Publ., 1999, pp. 481–497.
[4] Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs.
Tools and Algo-
rithms for the Construction and Analysis of Systems
(
TACAS 2004
). Ed. by K. Jensen,
A. Podelski. Vol. 2988 of Lecture Notes in Computer Science. Springer, 2004, pp. 168–176.
[5] Clarke E., Grumberg O., Jha S. et al. Counterexample-guided abstraction refinement.
Com-
puter Aided Verification
, 2000, pp. 154–169.
[6] Henzinger T.A., Jhala R., Majumdar R., Sutre G. Software verification with blast.
10th SPIN
Workshop on Model Checking Software
(
SPIN
). LNCS 2648. Springer-Verlag, 2003,
pp. 235–239.
[7] Cousot P. Abstract interpretation. ACM Computing Surveys (CSUR).
ACM
. N.Y., 1996,
vol. 28, iss. 2, pp. 324–328.
[8] Glukhikh M.I., Itsykson V.M., Tsesko V.A. The use of dependencies for improving the
precision of program static analysis.
Model. Anal. Inform. Sist
., 2011, vol. 18, no. 4, pp. 68–79.
[9] Holzmann G., Peled D. An improvement in formal verification.
FORTE 1994 Conference
,
1994, pp. 197–211.
[10] Gerth R., Kuiper R., Peled D., Penczek W. A partial order approach to branching time
logic model checking.
Inf. Comput
., 1999, vol. 150, no. 2, pp. 132–152.
[11] Penczek W., Szreter M., Gerth R., Kuiper R. Partial order reductions preserving simula-
tions.
Proc. of Concurrency, Specification and Programming
(
CSP’99
)
.
Warsaw, 1999,
pp. 153–172.
[12] Holzmann G.J. An analysis of bitstate hashing.
Formal methods in system design
, 1998,
vol. 13, no. 3, pp. 287–307.
[13] Holzmann G.J. The spin model checker: Primer and Reference Manual. Addison-Wesley,
2003. 608 p.