Advertisement

Program Verification by Using DISCOVERER

  • Lu Yang
  • Naijun Zhan
  • Bican Xia
  • Chaochen Zhou
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4171)

Abstract

Recent advances in program verification indicate that various verification problems can be reduced to semi-algebraic system (SAS for short) solving. An SAS consists of polynomial equations and polynomial inequalities. Algorithms for quantifier elimination of real closed fields are the general method for those problems. But the general method usually has low efficiency for specific problems. To overcome the bottleneck of program verification with a symbolic approach, one has to combine special techniques with the general method. Based on the work of complete discrimination systems of polynomials [33,31],, we invented new theories and algorithms [32,30,35] for SAS solving and partly implemented them as a real symbolic computation tool in Maple named DISCOVERER. In this paper, we first summarize the results that we have done so far both on SAS-solving and program verification with DISCOVERER, and then discuss the future work in this direction, including SAS-solving itself, termination analysis and invariant generation of programs, and reachability computation of hybrid systems etc.

Keywords

semi-algebraic systems DISCOVERER program verification termination invariant generation reachability computation 

References

  1. 1.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(3), 3–34 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of Polynomial Programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)Google Scholar
  4. 4.
    Clark, E.M., Emerson, A., Sistla, A.P.: Automatic verification of finite-state concurrent programs using temporal logic. ACM Transaction on Programming Languages and Systems 8(2), 244–263 (1986)CrossRefzbMATHGoogle Scholar
  5. 5.
    Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, Springer, Heidelberg (1981)Google Scholar
  6. 6.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  7. 7.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)Google Scholar
  8. 8.
    Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. of Symbolic Computation 12, 299–328 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    colón, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    colón, M., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 67–81. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Cousot, P., Cousot, R.: Abstraction interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPL 1977, pp. 238–252 (1977)Google Scholar
  12. 12.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM POPL 1979, pp. 269–282 (1979)Google Scholar
  13. 13.
    Damas, L., Milner, R.: Principal type-schemes for functional programs. In: ACM POPL 1982, pp. 207–212 (1982)Google Scholar
  14. 14.
    Davenport, J.H., Heintz, J.: Real Elimination is Doubly Exponential. J. of Symbolic Computation 5, 29–37 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Dolzman, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9Google Scholar
  16. 16.
    Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretation complete. J. ACM 4792, 361–416 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. of Computer Science and System Sciences 57, 94–124 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Lafferrierre, G., Pappas, G.J., Yovine, S.: Symbolic reachability computaion for families of linear vector fields. J. of Symbolic Computation 11, 1–23 (2001)Google Scholar
  19. 19.
    Milner, R.: A theory of polymorphism in programming. J. Computer System Science 17(3), 348–375 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: A protype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)Google Scholar
  21. 21.
    Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system Coq. J. Symbolic Logic 15(5/6), 607–640 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Puri, A., Varaiya, P.: Decidability of hybrid systems with rectangular differential inclusions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 95–104. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  23. 23.
    Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  24. 24.
    Queille, J.-P., Sifakis, J.: Verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  25. 25.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: ACM POPL 2004, pp. 318–329 (2004)Google Scholar
  26. 26.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539–554. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  27. 27.
    Tarski, A.: A Decision for Elementary Algebra and Geometry, May 1951. University of California Press, Berkeley (1951)zbMATHGoogle Scholar
  28. 28.
    Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  29. 29.
    Wang, D., Xia, B.: Stability analysis of biological systems with real solution classification. In: Kauers, M. (ed.) Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation (ISSAC 2005), pp. 354–361. ACM Press, New York (2005)CrossRefGoogle Scholar
  30. 30.
    Xia, B., Yang, L.: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symbolic Computation 34, 461–477 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Yang, L.: Recent advances on determining the number of real roots of parametric polynomials. J. Symbolic Computation 28, 225–242 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Yang, L., Hou, X., Xia, B.: A complete algorithm for automated discovering of a class of inequality-type theorems. Sci. in China (Ser. F) 44, 33–49 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Yang, L., Hou, X., Zeng, Z.: A complete discrimination system for polynomials. Science in China (Ser. E) 39, 628–646 (1996)MathSciNetzbMATHGoogle Scholar
  34. 34.
    Yang, L., Xia, B.C.: An explicit criterion to determine the number of roots of a polynomial on an interval. Progress in Natural Science 10(12), 897–910 (2000)MathSciNetGoogle Scholar
  35. 35.
    Yang, L., Xia, B.: Real solution classifications of a class of parametric semi-algebraic systems. In: Proc. of Int’l Conf. on Algorithmic Algebra and Logic, pp. 281–289 (2005)Google Scholar
  36. 36.
    Yang, L., Zhang, J., Hou, X.: A criterion of dependency between algebraic equations and its applications. In: Wen-tsun, W., de Cheng, M.- (eds.) Proceedings of International Workshop on Mathematics Mechanization 1992, pp. 110–134. International Academic Publishers, Beijing (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Lu Yang
    • 1
  • Naijun Zhan
    • 2
  • Bican Xia
    • 3
  • Chaochen Zhou
    • 2
  1. 1.Software Engineering InstituteEast China Normal UniversityChina
  2. 2.Laboratory of Computer Science,Institute of SoftwareAcademia SinicaChina
  3. 3.LMAM & School of Mathematical SciencesPeking UniversityChina

Personalised recommendations