Abstract
We present a symbolic-numeric hybrid method, based on sum-of-squares (SOS) relaxation and rational vector recovery, to compute inequality invariants and ranking functions for proving total correctness and generating preconditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate ranking functions with floating point coefficients. Then Gauss-Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several examples are given to show the effectiveness of our method.
| Original language | English |
|---|---|
| Pages (from-to) | 192-202 |
| Number of pages | 11 |
| Journal | Frontiers of Computer Science |
| Volume | 8 |
| Issue number | 2 |
| DOIs | |
| State | Published - Apr 2014 |
Keywords
- precondition generation
- semidefinite programming
- sum-of-squares relaxation
- symbolic computation
- total correctness
Fingerprint
Dive into the research topics of 'Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver