Skip to main content
SpringerLink
Log in

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

  • Cybernetics
  • Published:
Cybernetics and Systems Analysis Aims and scope

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  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.

  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.

  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).

  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.

  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.

  6. P. Cousot, “Verification by abstract interpretation,” Lecture Notes in Comput. Sci., No. 2772, 243–268 (2003).

  7. F. Nielson, “A denotation framework for data flow analysis,” Acta Informatica, No. 18, 265–287 (1982).

  8. F. Nielson, “Two-level semantics and abstract interpretation,” Theor. Comput. Sci. (Fundamental Studies), No. 69, 117–242 (1989).

  9. N. D. Jones, C. K. Gomard, and P. Sestoft, Partial Evaluation and Automatic Program Generation, Techn. Un-ty of Denmark (1993).

  10. G. D. Birkhoff, Lattice Theory [Russian translation], Nauka, Moscow (1984).

    Google Scholar 

  11. P. Cousot and R. Cousot, “Abstract interpretation frameworks,” Journ. of Logic and Comput., 2, No. 4, 511–547 (1992).

    Article  MathSciNet  MATH  Google Scholar 

  12. P. Cousot and R. Cousot, “Modular static program analysis (invited paper),” Lecture Notes in Comput. Sci., No. 2304, 159–178 (2002).

  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.

  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.

  15. S. L. Krivoi and S. G. Raksha, “Search for invariant linear relationships in programs,” Cybernetics, 20, No. 6, 796–803 (1984).

    Article  MathSciNet  Google Scholar 

  16. S. L. Krivoi, “An algorithm for finding invariant relations in programs,” Cybernetics, 17, No. 5, 582–589 (1981).

    Article  MathSciNet  Google Scholar 

  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.

  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.

  19. P. Cousot, “Abstract interpretation based formal methods and future challenges,” Lecture Notes in Comput. Sci., Vol. 2000, 138-156 (2001).

  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).

Download references

Author information

Authors and Affiliations

  1. Taras Shevchenko National University of Kyiv, Kyiv, Ukraine

    S. L. Kryvyi & O. M. Maksymets

Authors
  1. S. L. Kryvyi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. O. M. Maksymets
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to S. L. Kryvyi.

Additional information

Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 3–14, November–December 2013.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Kryvyi, S.L., Maksymets, O.M. Program Verification: State of the Art, Problems, and Results. I. Cybern Syst Anal 49, 805–814 (2013). https://doi.org/10.1007/s10559-013-9569-1

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10559-013-9569-1

Keywords

Search

Navigation