Recent advances in program verification through computer algebra

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