Abstract
This paper investigates how to apply the techniques on solving semi-algebraic systems to invariant generation of polynomial programs. By our approach, the generated invariants represented as a semi-algebraic system are more expressive than those generated with the well-established approaches in the literature, which are normally represented as a conjunction of polynomial equations. We implement this approach with the computer algebra tools DISCOVERER and QEPCAD. We also explain, through the complexity analysis, why our approach is more efficient and practical than the one of [17] which directly applies first-order quantifier elimination.
This work is supported in part by NKBRPC-2002cb312200, NKBRPC-2004CB318003, NSFC-60493200, NSFC-60421001, NSFC-60573007, and NKBRPC-2005CB321902.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Besson, F., Jensen, T., Talpin, J.-P.: Polyhedral analysis of synchronous languages. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 51–69. Springer, Heidelberg (1999)
Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: ICTAC 2007. LNCS, Springer, Heidelberg (2007) (invited paper)
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. 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)
Cousot, P.: Proving program invariance and termination by parametric abstraction, Langrangian Relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: ACM POPL 1978, pp. 84–97 (1978)
Davenport, J.H., Heintz, J.: Real Elimination is Doubly Exponential. J. of Symbolic Computation 5, 29–37 (1988)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Dolzman, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9
Floyd, R.W.: Assigning meanings to programs. In: Proc. Symphosia in Applied Mathematics, vol. 19, pp. 19–37 (1967)
Gallo, G., Mishra, B.: Efficient Algorithms and Bounds for Wu-Ritt Characteristic Sets. In: Mora, T., Traverso, C. (eds.) Effective methods in algebraic geometry, Birkhäuser, Bosten. Progress in Mathematics, pp. 119–142 (1994)
German, S., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Transactions on Software Engineering 1(1), 68–75 (1975)
Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576–580 (1969)
Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)
Katz, S., Manna, Z.: Logical analysis of programms. Communications of the ACM 19(4), 188–206 (1976)
Kapur, D.: Automatically generating loop invariants using quantifier llimination. In: Proc. IMACS Intl. Conf. on Applications of Computer Algebra ( ACA 2004), Beaumont, Texas (July 2004)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)
Múller-Olm, M., Seidl, H.: Polynomial constants are decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 4–19. Springer, Heidelberg (2002)
Múller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: ACM SIGPLAN Principles of Programming Languages, POPL 2004, pp. 330–341 (2004)
Rodriguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 280–295. Springer, Heidelberg (2004)
Rodriguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: Proc. Intl. Symp on Symbolic and Algebraic Computation (ISSAC 2004) (July 2004)
Rodriguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation 42, 443–476 (2007)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: ACM POPL 2004, pp. 318–329 (2004)
Wegbreit, B.: The synthesis of loop predicates. Communications of the ACM 17(2), 102–112 (1974)
Wu, W.-T.: Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. 4, 207–235 (1984)
Xia, B., Xiao, R., Yang, L.: Solving parametric semi-algebraic systems. In: Pae, S.-l, Park, H. (eds.) Proc. the 7th Asian Symposium on Computer Mathematics (ASCM 2005), Seoul, December 8-10, pp. 153–156 (2005)
Xia, B., Yang, L.: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symbolic Computation 34, 461–477 (2002)
Xia, B., Zhang, T.: Real Solution Isolation Using Interval Arithmetic. Comput. Math. Appl. 52, 853–860 (2006)
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.: Automated Deduction in Real Geometry. In: Chen, F., Wang, D. (eds.) Geometric Computation, pp. 248–298. World Scientific, Singapore (2004)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Chen, Y., Xia, B., Yang, L., Zhan, N. (2007). Generating Polynomial Invariants with DISCOVERER and QEPCAD. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Formal Methods and Hybrid Real-Time Systems. Lecture Notes in Computer Science, vol 4700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75221-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-75221-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75220-2
Online ISBN: 978-3-540-75221-9
eBook Packages: Computer ScienceComputer Science (R0)