Content area
Abstract
In this paper, we summarize the results on program verification through semi-algebraic systems (SASs) 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.
Details
Title
Recent advances in program verification through computer algebra
Author
Yang, Lu 1 ; Zhou, Chaochen 2 ; Zhan, Naijun 2 ; Xia, Bican 3
1 East China Normal University, Laboratory of Trustworthy Computing, Shanghai, China (GRID:grid.22069.3f) (ISNI:0000000403696365)
2 Chinese Academy of Sciences, Laboratory of Computer Science, Institute of Software, Beijing, China (GRID:grid.9227.e) (ISNI:0000000119573309)
3 Peking University, LMAM & School of Mathematical Sciences, Beijing, China (GRID:grid.11135.37) (ISNI:0000000122569319)
1 East China Normal University, Laboratory of Trustworthy Computing, Shanghai, China (GRID:grid.22069.3f) (ISNI:0000000403696365)
2 Chinese Academy of Sciences, Laboratory of Computer Science, Institute of Software, Beijing, China (GRID:grid.9227.e) (ISNI:0000000119573309)
3 Peking University, LMAM & School of Mathematical Sciences, Beijing, China (GRID:grid.11135.37) (ISNI:0000000122569319)
Pages
1-16
Publication year
2010
Publication date
Mar 2010
ISSN
16737350
e-ISSN
16737466
Source type
Scholarly Journal
Language of publication
English
ProQuest document ID
2918720177
Copyright
© Higher Education Press and Springer Berlin Heidelberg 2010.