%A Lu YANG, Chaochen ZHOU, Naijun ZHAN, Bican XIA, %T Recent advances in program verification through computer algebra %0 Journal Article %D 2010 %J Front. Comput. Sci. %J Frontiers of Computer Science %@ 2095-2228 %R 10.1007/s11704-009-0074-7 %P 1-16 %V 4 %N 1 %U {https://journal.hep.com.cn/fcs/EN/10.1007/s11704-009-0074-7 %8 2010-03-05 %X In this paper, we summarize the results on program verification through semi-algebraic systemsSASs solving that we have obtained, including automatic discovery of invariants and ranking functions, symbolic decision procedure for the termination of a class of linear loops, termination analysis of nonlinear systems, and so on.