Proving termination of nonlinear command sequences.
Saved in:
| 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 |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 87478403 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Proving termination of nonlinear command sequences. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Babić%2C+Domagoj%22">Babić, Domagoj</searchLink><relatesTo>1</relatesTo><i> babic.domagoj@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Cook%2C+Byron%22">Cook, Byron</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22Hu%2C+Alan%22">Hu, Alan</searchLink><relatesTo>3</relatesTo><br /><searchLink fieldCode="AR" term="%22Rakamarić%2C+Zvonimir%22">Rakamarić, Zvonimir</searchLink><relatesTo>4</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Formal+Aspects+of+Computing%22">Formal Aspects of Computing</searchLink>. May2013, Vol. 25 Issue 3, p389-403. 15p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Nonlinear+assignment+problems%22">Nonlinear assignment problems</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+termination%22">Computer software termination</searchLink><br /><searchLink fieldCode="DE" term="%22Divergence+theorem%22">Divergence theorem</searchLink><br /><searchLink fieldCode="DE" term="%22Nonlinear+analysis%22">Nonlinear analysis</searchLink><br /><searchLink fieldCode="DE" term="%22Loops+%28Group+theory%29%22">Loops (Group theory)</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=87478403 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s00165-012-0252-5 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 15 StartPage: 389 Subjects: – SubjectFull: Nonlinear assignment problems Type: general – SubjectFull: Computer software termination Type: general – SubjectFull: Divergence theorem Type: general – SubjectFull: Nonlinear analysis Type: general – SubjectFull: Loops (Group theory) Type: general Titles: – TitleFull: Proving termination of nonlinear command sequences. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Babić, Domagoj – PersonEntity: Name: NameFull: Cook, Byron – PersonEntity: Name: NameFull: Hu, Alan – PersonEntity: Name: NameFull: Rakamarić, Zvonimir IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 05 Text: May2013 Type: published Y: 2013 Identifiers: – Type: issn-print Value: 09345043 Numbering: – Type: volume Value: 25 – Type: issue Value: 3 Titles: – TitleFull: Formal Aspects of Computing Type: main |
| ResultId | 1 |
