Program Verification Through Computer Algebra

  • Zhou Chaochen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


This is to advocate the approach to reducing program verification to the algebraic symbolic computation. Recent advances indicate that various verification problems can be reduced to semi-algebraic systems (SAS for short), and resolved through computer algebra tools. In this talk, we report our encouraging attempts at applying DISCOVERER to program termination analysis and state reachability computation. DISCOVERER is a Maple program implementing an algorithm of real solution classification and isolation for SAS, which is based on the discovery of complete discrimination systems of parametric polynomials. The talk also concludes that this approach deserves further attention from the program verification community.

For theoretical and technical details of the work, we refer the reader to [1,2,3,4,5].


Operating System Software Engineer Technical Detail Real Root Science Institute 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Xia, B., Yang, L.: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symbolic Computation 34, 461–477 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Yang, L.: Recent advances on determining the number of real roots of parametric polynomials. J. Symbolic Computation 28, 225–242 (1999)zbMATHCrossRefGoogle Scholar
  3. 3.
    Yang, L., Hou, X., Zeng, Z.: A complete discrimination system for polynomials. Science in China (Ser. E) 39, 628–646 (1996)zbMATHMathSciNetGoogle Scholar
  4. 4.
    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
  5. 5.
    Yang, L., Zhan, N., Xia, B., Zhou, C.: Program verification by using DISCOVERER. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 528–538. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Zhou Chaochen
    • 1
  1. 1.Laboratory of Computer ScienceInstitute of Software, Chinese Academy of SciencesBeijingChina

Personalised recommendations