Skip to main content
SpringerLink
Log in

Generating Polynomial Invariants with DISCOVERER and QEPCAD

  • Chapter
Formal Methods and Hybrid Real-Time Systems

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4700))

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.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  4. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. of Symbolic Computation 12, 299–328 (1991)

    MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  7. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: ACM POPL 1978, pp. 84–97 (1978)

    Google Scholar 

  8. Davenport, J.H., Heintz, J.: Real Elimination is Doubly Exponential. J. of Symbolic Computation 5, 29–37 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  9. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  10. Dolzman, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9

    Google Scholar 

  11. Floyd, R.W.: Assigning meanings to programs. In: Proc. Symphosia in Applied Mathematics, vol. 19, pp. 19–37 (1967)

    Google Scholar 

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

    Google Scholar 

  13. German, S., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Transactions on Software Engineering 1(1), 68–75 (1975)

    Google Scholar 

  14. Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  15. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  16. Katz, S., Manna, Z.: Logical analysis of programms. Communications of the ACM 19(4), 188–206 (1976)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  18. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  23. Rodriguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation 42, 443–476 (2007)

    Article  MATH  MathSciNet  Google Scholar 

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

  25. Wegbreit, B.: The synthesis of loop predicates. Communications of the ACM 17(2), 102–112 (1974)

    Article  MATH  MathSciNet  Google Scholar 

  26. Wu, W.-T.: Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. 4, 207–235 (1984)

    Google Scholar 

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

    Google Scholar 

  28. Xia, B., Yang, L.: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symbolic Computation 34, 461–477 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  29. Xia, B., Zhang, T.: Real Solution Isolation Using Interval Arithmetic. Comput. Math. Appl. 52, 853–860 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  30. Yang, L.: Recent advances on determining the number of real roots of parametric polynomials. J. Symbolic Computation 28, 225–242 (1999)

    Article  MATH  Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  32. Yang, L., Hou, X., Zeng, Z.: A complete discrimination system for polynomials. Science in China (Ser. E) 39, 628–646 (1996)

    MATH  MathSciNet  Google Scholar 

  33. Yang, L., Xia, B.: Automated Deduction in Real Geometry. In: Chen, F., Wang, D. (eds.) Geometric Computation, pp. 248–298. World Scientific, Singapore (2004)

    Google Scholar 

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

Download references

Author information

Authors and Affiliations

  1. LMAM & School of Mathematical Sciences, Peking University,  

    Yinghua Chen & Bican Xia

  2. Institute of Theoretical Computing, East China Normal University,  

    Lu Yang

  3. Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, South Fourth Street, No. 4, Zhong Guan Cun, Beijing, 100080, P.R. China

    Naijun Zhan

Authors
  1. Yinghua Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bican Xia
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lu Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Naijun Zhan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Cliff B. Jones Zhiming Liu Jim Woodcock

Rights and permissions

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

Publish with us

Policies and ethics

Search

Navigation