Recent advances in program verification through
computer algebra

doi:10.1007/s11704-009-0074-7

PDF(255 KB)

Front. Comput. Sci. ›› 2010, Vol. 4 ›› Issue (1) : 1-16. DOI: 10.1007/s11704-009-0074-7

Research articles

Recent advances in program verification through computer algebra

Lu YANG¹,Chaochen ZHOU²,Naijun ZHAN²,Bican XIA³,

Author information +

History +

Abstract

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.

Keywords

program verification / computer algebra / semi-algebraic systems solving / embedded systems / invariants / ranking functions / termination

Cite this article

EndNote

Ris (Procite)

Bibtex

Download citation ▾

Lu YANG, Chaochen ZHOU, Naijun ZHAN, Bican XIA,. Recent advances in program verification through computer algebra. Front. Comput. Sci., 2010, 4(1): 1‒16 https://doi.org/10.1007/s11704-009-0074-7