Abstract
This paper is devoted of analysis of a work of Burgstaller B., Scholz B. and Blieberger J. about program transformation into symbolic domain for future analysis. There is mathematical apparatus for a program description in the terms of symbolic computation in the paper: authors suggest using terms of context, program state, and super-context for formulas program description. There are examples of transformation of a program to symbolic domain. Proposed approach of loops description is a main achievement of this work. That way allows getting formal cycle representation and reducing potentially infinite number of ways to the end of the program.

Examples of operation of the original source areanalyzed, but, and this is certainly a drawback of the original work, all the examples are quite simple, and does not contain more than 8 lines, which ultimately leads to that it is impossible to draw a conclusion about the applicability of the method.

During the analysis of the study work has identified a number of shortcomings: 1) the method of "folding" the number of paths in a loop does not result in the claimed if the cycle is branching; 2) is not obvious how it will look proposed a formal description of the cycles in the case of nested loops. And in cycles with a large number of nesting should be based on the iterable variables, ie expression of the form: a[i][j] = b[i][j] or the like; 3) there is no description of the character representation for arrays and is especially important to iterate over the array elements in cycles in the form of a[i].

 

References
1. Burgstaller B., Scholz B., Blieberger J. A symbolic analysis framework for static analysis of imperative programming languages. Journal of Systems and Software, 2012, vol. 85, iss. 6, pp. 1418–1439. doi: 10.1016/j.jss.2011.11.1039

2. Tarjan R.E. A unified approach to path problems. Journal of the ACM (JACM), 1981, vol. 28, iss. 3, pp. 577–593. doi: 10.1145/322261.322272

3. Hecht M.S. Flow analysis of compute programs. New York, Elsevier, North Holland, 1977. 232 p.

4. Voevoda A.A., Romannikov D.O. O metode analiza programm [About the method of program analysis]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2014, no. 4 (78), pp. 125–138. doi: 10.17212/2307-6879-2014-4-125-138

5. Voevoda A.A., Romannikov D.O. Sposoby predstavleniya programm i ikh analiz [Methods of program representation and analysis]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2014, no. 3 (76),

pp. 81–98.

6. Romannikov D.O. O poiske vkhodnykh intervalov [On the search for input intervals]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2014, no. 1 (75), pp. 140–145.

7. Abramsky S., Hankin C. An introduction to abstract interpretation. Available at: https://www.cs.virginia.edu/~weimer/2007-615/reading/AbramskiAI.pdf (accessed 20.04.2015)

8. Cousot P., Cousot R. A gentle introduction to formal verification of computer systems by abstract interpretation. NATO Science Series – D: Information and Communication Security. Vol. 25: Logics and Languages for Reliability and Security. Amsterdam, IOS Press, 2010, pp. 1–29. doi: 10.3233/978-1-60750-100-8-1.

9. Glukhikh M.I., Itsykson V.M., Tses'ko V.A. Ispol'zovanie zavisimostei dlya povysheniya tochnosti staticheskogo analiza programm [Using dependencies to improve precision of code analysis]. Modelirovanie i analiz informatsionnykh sistem – Modeling and Analisys of Information System, 2011, vol. 18, no. 4,

pp. 68–79.

10. Bush W.R., Pincus J.D., Sielaff D.J. A static analyzer for finding dynamic programming errors. Software: Practice and Experience, 2000, vol. 30, iss. 7,

pp. 775–802. doi: 10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H

11. Clarke E.M., Grumberg O., Peled D. Model checking. Cambridge, London, MIT Press, 2001 (Russ. ed.: Klark E., Gramberg O., Peled D. Verifikatsiya modelei programm: Model checking. Moscow, MTsNMO Publ., 2002. 416 p.).

12. Karpov Yu.G. Model Checking. Verifikatsiya parallel'nykh i raspredelennykh programmnykh sistem [Model Checking. Verification of parallel and distributed software systems]. St. Petersburg, BHV-Petersburg Publ., 2010. 560 p.

13. Horwitz S., Reps T., Binkley D. Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems, 1990, vol. 12, iss. 1, pp. 26–60. doi: 10.1145/77606.77608

14. Ferrante J., Ottenstein K.J., Warren J.D. The program dependence graph and its use in optimization. ACM Transactions on Programming Languages and Systems (TOPLAS), 1987, vol. 9, iss. 3, pp. 319–349. doi: 10.1145/24039.24041

15. Voevoda A.A., Markov A.V., Romannikov D.O. Razrabotka program-mnogo obespecheniya: proektirovanie s ispol'zovaniem UML diagramm i setei Petri na primere ASU TP vodonapornoi stantsii [Software development: software design using UML diagrams and Petri nets for example automated process control system of pumping station]. Trudy SPIIRAN – SPIIRAS Proceedings, 2014, iss. 3 (34),

pp. 218–231.

16. Romannikov D.O. Nakhozhdenie oshibok obrashcheniya k nesushchest-vuyushchim elementam massiva na osnovanii rezul'tatov analiza seti Petri [Finding errors or nonexistent array’s elements based on the results of the analysis Petri nets]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2012, no. 1 (67), pp. 115–120.

17. Markov A.V., Romannikov D.O. Algoritm translyatsii diagrammy aktivnosti v set' Petri [Algorithm of automatic conversion of the activity diagram into petri-net structure formats]. Doklady Akademii nauk vysshei shkoly Rossiiskoi Federatsii – Proceedings of the Russian higher school Academy of sciences, 2014, no. 1 (22), pp. 104–112.

18. Voevoda A.A., Romannikov D.O. Redutsirovanie prostranstva sostoyanii seti Petri dlya ob"ektov iz odnogo klassa [Reducing the state space of Petri nets for objects of one class]. Nauchnyi vestnik Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Science bulletin of the Novosibirsk state technical university, 2011, no. 4 (45), pp. 146–150.

19. Romannikov D.O., Markov A.V., Zimaev I.V. Obzor rabot, posvyashchennykh razrabotke PO s ispol'zovaniem UML i setei Petri [The review of works devoted to development of the software with use UML and Petri nets]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2011, no. 1 (63), pp. 91–104.

20. Markov A.V. Analiz otdel'nykh chastei dereva dostizhimosti setei Petri [Analysis of individual pieces of wood reachability Petri nets]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2013, no. 3 (73), pp. 58–74.

21. Voevoda A.A., Markov A.V. Rekursiya v setyakh Petri [The concepts recursion in Petri net]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2012, no. 3 (69), pp. 115–122.

22. Voevoda A.A., Markov A.V. Testirovanie UML-diagramm s pomoshch'yu apparata setei Petri na primere razrabotki po dlya igry "Zmeika" [About testing UML-diagrams by means of the device of Petri nets on the example of software engineering for game "Snake"]. Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2010, no. 3 (61), pp. 51–60.

23. Voevoda A.A., Zimaev I.V. Verifikatsiya workflow-modelei s primeneniem setei Petri [Verification of workflow-models using Petri-nets]. Nauchnyi vestnik Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Science bulletin of the Novosibirsk state technical university, 2010, no. 4 (41), pp. 151–154.

24. Voevoda A.A., Sarkenov D.O., Khassounekh V. Modelirovanie protokolov s uchetom vremeni na tsvetnykh setyakh Petri [Protocol modeling with regards of time on colored Petri nets] Sbornik nauchnyh trudov Novosibirskogo gosudarstvennogo tekhnicheskogo universiteta – Transaction of scientific papers of the Novosibirsk state technical university, 2004, no. 3 (37), pp. 133–136.