Synthetic Software Verification Method using SMT-Solvers

Non-deterministic behavior of the software remains a pressing issue. Software verification aims to detect errors, identify vulnerabilities and check whether the required features are implemented correctly. Verification methods can be divided into groups: the empirical (using review), formal (using mathematics for software verification), static (checking the software implementation without immediate start), dynamic (checking the software 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 synthetic 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 Academic Publ., 1999, pp. 481-497.

[4] Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. Tools and Algorithms 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. Computer 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 simulations. 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.

[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 using a compiler IR. Institute for Theoretical Computer Science Karlsruhe Institute of Technology (KIT). Germany, 2012. 16 p.