Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Practical Methods for Proving Program Termination
| |
|
Practical Methods for Proving Program Termination
Michael A. Colón6  and Henny B. Sipma6
| (6) |
Computer Science Department, Stanford University, Stanford, CA, 94305-9045 |
Abstract
We present two algorithms to prove termination of programs by synthesizing linear ranking functions. The first uses an invariant
generator based on iterative forward propagation with widening and extracts ranking functions from the generated invariants
by manipulating polyhedral cones. It is capable of finding subtle ranking functions which are linear combinations of many
program variables, but is limited to programs with few variables.
The second, more heuristic, algorithm targets the class of structured programs with single-variable ranking functions. Its
invariant generator uses a heuristic extrapolation operator to avoid iterative forward propagation over program loops. For
the programs we have considered, this approach converges faster and the invariants it discovers are sufficiently strong to
imply the existence of ranking functions.
This research was supported in part by NSF(ITR) grant CCR-01-21403, by NSF grant CCR-99-00984-001, by ARO grant DAAD19-01-1-0723,
and by ARPA/AF contracts F33615-00-C-1693 and F33615-99-C-3014.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|