Cybernetics and Systems Analysis

, Volume 49, Issue 6, pp 805–814 | Cite as

Program Verification: State of the Art, Problems, and Results. I

  • S. L. Kryvyi
  • O. M. Maksymets


An analytical survey of modern verification methods for sequential functional, reactive, and distributed systems is presented. The emphasis is on methods based on properties of abstract interpretation, transition systems, and Petri nets.


verification abstract interpretation transition system Petri net model checking 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. N. Maksimets, “Searching for program invariants in the form of polynomials,” in: Proc. National Academy of Sciences of Ukraine, Vol. 9, (2013), pp. 44–50.Google Scholar
  2. 2.
    S. L. Kryvyi and A. N. Maksimets, “Formal verification methods based on Petri nets,” in: Proc. 10th Intern. Conf. “Theoretical and applied aspects of program construction. Systems TAAbD’2013,” Yalta (2013), pp. 75–80.Google Scholar
  3. 3.
    F. Sintzoff, “Calculating properties of programs by variations on specific models,” in: ACM Conf. on Proving Assertions about Programs, Sigplan Notices, 7, No. 1, 203–207 (1972).Google Scholar
  4. 4.
    P. Cousot, “Semantic foundations of program analysis,” in: S. S. Muchnik and N. D. Jones (eds.), Program Flow Analysis: Theory and Applications, 10, Prentice-Hall (1981), pp. 303–342.Google Scholar
  5. 5.
    P. Cousot, “Abstract interpretation: A unified lattice model for static analysis of programs by construction of fixpoints,” in: Proc. 4th ACM Symposium on Principles of Programming Languages, ACM, Los Angeles (1977), pp. 238–252.Google Scholar
  6. 6.
    P. Cousot, “Verification by abstract interpretation,” Lecture Notes in Comput. Sci., No. 2772, 243–268 (2003).Google Scholar
  7. 7.
    F. Nielson, “A denotation framework for data flow analysis,” Acta Informatica, No. 18, 265–287 (1982).Google Scholar
  8. 8.
    F. Nielson, “Two-level semantics and abstract interpretation,” Theor. Comput. Sci. (Fundamental Studies), No. 69, 117–242 (1989).Google Scholar
  9. 9.
    N. D. Jones, C. K. Gomard, and P. Sestoft, Partial Evaluation and Automatic Program Generation, Techn. Un-ty of Denmark (1993).Google Scholar
  10. 10.
    G. D. Birkhoff, Lattice Theory [Russian translation], Nauka, Moscow (1984).Google Scholar
  11. 11.
    P. Cousot and R. Cousot, “Abstract interpretation frameworks,” Journ. of Logic and Comput., 2, No. 4, 511–547 (1992).MathSciNetCrossRefMATHGoogle Scholar
  12. 12.
    P. Cousot and R. Cousot, “Modular static program analysis (invited paper),” Lecture Notes in Comput. Sci., No. 2304, 159–178 (2002).Google Scholar
  13. 13.
    E. Rodriguez-Carbonell and D. Kapur, “An abstract interpretation approach for automatic generation of polynomial invariants,” in: Proc. Static Analysis Symposium (SAS), Italy (2004), pp. 1–8.Google Scholar
  14. 14.
    M. S. Lvov, “About one algorithm of program polynomial invariants generation,” in: M. Giese and T. Jebelean (eds.), Proc. Workshop on Invariant Generation, Techn. Rep. No. 0707 (RISC Rep. Ser.), Univ. of Linz, Linz, Austria (2007), pp. 85–99.Google Scholar
  15. 15.
    S. L. Krivoi and S. G. Raksha, “Search for invariant linear relationships in programs,” Cybernetics, 20, No. 6, 796–803 (1984).MathSciNetCrossRefGoogle Scholar
  16. 16.
    S. L. Krivoi, “An algorithm for finding invariant relations in programs,” Cybernetics, 17, No. 5, 582–589 (1981).MathSciNetCrossRefGoogle Scholar
  17. 17.
    G. A. Kildall, “A unified approach to global program optimization,” in: Proc. ACM Symp. on Principles of Program Languages, Boston, MA (1973), pp. 194–206.Google Scholar
  18. 18.
    P. Cousot, “Abstract interpretation perspective,” in: ACM Workshop on Strategic Directions in Comput. Res., MIT Laboratory for Comput. Sci., Cambridge, Massachusetts, USA (1996), pp. 1–8.Google Scholar
  19. 19.
    P. Cousot, “Abstract interpretation based formal methods and future challenges,” Lecture Notes in Comput. Sci., Vol. 2000, 138-156 (2001).Google Scholar
  20. 20.
    B. Saddek, S. Graf, and Y. Lakhnech, “Abstraction as the key for invariant verification,” Lecture Notes in Comput. Sci., No. 2772, 67–99 (2003).Google Scholar

Copyright information

© Springer Science+Business Media New York 2013

Authors and Affiliations

  1. 1.Taras Shevchenko National University of KyivKyivUkraine

Personalised recommendations