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.
This work is supported in part by NKBRPC-2002cb312200, NKBRPC-2004CB318003, NSFC-60273022, NSFC-60493200, NSFC-60421001, NSFC-60573007, and NKBRPC-2005CB321902.
Chapter PDF
Similar content being viewed by others
Keywords
References
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)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of Polynomial Programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)
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)
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)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
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)
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. of Symbolic Computation 12, 299–328 (1991)
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)
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)
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)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM POPL 1979, pp. 269–282 (1979)
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: ACM POPL 1982, pp. 207–212 (1982)
Davenport, J.H., Heintz, J.: Real Elimination is Doubly Exponential. J. of Symbolic Computation 5, 29–37 (1988)
Dolzman, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretation complete. J. ACM 4792, 361–416 (2000)
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)
Lafferrierre, G., Pappas, G.J., Yovine, S.: Symbolic reachability computaion for families of linear vector fields. J. of Symbolic Computation 11, 1–23 (2001)
Milner, R.: A theory of polymorphism in programming. J. Computer System Science 17(3), 348–375 (1978)
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)
Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system Coq. J. Symbolic Logic 15(5/6), 607–640 (1993)
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)
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)
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)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: ACM POPL 2004, pp. 318–329 (2004)
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)
Tarski, A.: A Decision for Elementary Algebra and Geometry, May 1951. University of California Press, Berkeley (1951)
Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70–82. Springer, Heidelberg (2004)
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)
Xia, B., Yang, L.: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symbolic Computation 34, 461–477 (2002)
Yang, L.: Recent advances on determining the number of real roots of parametric polynomials. J. Symbolic Computation 28, 225–242 (1999)
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)
Yang, L., Hou, X., Zeng, Z.: A complete discrimination system for polynomials. Science in China (Ser. E) 39, 628–646 (1996)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Yang, L., Zhan, N., Xia, B., Zhou, C. (2008). Program Verification by Using DISCOVERER. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_58
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_58
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)