Bibliographic Details
| Title: |
Proving termination of nonlinear command sequences. |
| Authors: |
Babić, Domagoj1 babic.domagoj@gmail.com, Cook, Byron2, Hu, Alan3, Rakamarić, Zvonimir4 |
| Source: |
Formal Aspects of Computing. May2013, Vol. 25 Issue 3, p389-403. 15p. |
| Subjects: |
Nonlinear assignment problems, Computer software termination, Divergence theorem, Nonlinear analysis, Loops (Group theory) |
| Abstract: |
We describe a simple and efficient algorithm for proving the termination of a class of loops with nonlinear assignments to variables. The method is based on divergence testing for each variable in the cone-of-influence of the loop's condition. The analysis allows us to automatically prove the termination of loops that cannot be handled using previous techniques. We also describe a method for integrating our nonlinear termination proving technique into a larger termination proving framework that depends on linear reasoning. [ABSTRACT FROM AUTHOR] |
|
Copyright of Formal Aspects of Computing is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
