Proving mutual termination.
Saved in:
| Title: | Proving mutual termination. |
|---|---|
| Authors: | Elenbogen, Dima1 edima@cs.technion.ac.il, Katz, Shmuel1 katz@cs.technion.ac.il, Strichman, Ofer2 ofers@ie.technion.ac.il |
| Source: | Formal Methods in System Design. Oct2015, Vol. 47 Issue 2, p204-229. 26p. |
| Subjects: | Computer software termination, Electronic data processing, Systems design, Computer science, System analysis |
| Abstract: | Two programs are said to be mutually terminating if they terminate on exactly the same inputs. We suggest inference rules and a proof system for proving mutual termination of a given pair of procedures $$\langle $$ $$f$$ , $$f'$$ $$\rangle $$ and the respective subprograms that they call under a free context. Given a (possibly partial) mapping between the procedures of the two programs, the premise of the rule requires proving that given the same arbitrary input in, f( in) and $$f'(in)$$ call procedures mapped in the mapping with the same arguments. A variant of this proof rule with a weaker premise allows to prove termination of one of the programs if the other is known to terminate. In addition, we suggest various techniques for battling the inherent incompleteness of our solution, including a case in which the interface of the two procedures is not identical, and a case in which partial equivalence (the equivalence of their input/output behavior) has only been proven for some, but not all, the outputs of the two given procedures. We present an algorithm for decomposing the verification problem of whole programs to that of proving mutual termination of individual procedures, based on our suggested inference rules. The reported prototype implementation of this algorithm is the first to deal with the mutual termination problem. [ABSTRACT FROM AUTHOR] |
| Copyright of Formal Methods in System Design is the property of Springer Nature 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: 109575817 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Proving mutual termination. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Elenbogen%2C+Dima%22">Elenbogen, Dima</searchLink><relatesTo>1</relatesTo><i> edima@cs.technion.ac.il</i><br /><searchLink fieldCode="AR" term="%22Katz%2C+Shmuel%22">Katz, Shmuel</searchLink><relatesTo>1</relatesTo><i> katz@cs.technion.ac.il</i><br /><searchLink fieldCode="AR" term="%22Strichman%2C+Ofer%22">Strichman, Ofer</searchLink><relatesTo>2</relatesTo><i> ofers@ie.technion.ac.il</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Formal+Methods+in+System+Design%22">Formal Methods in System Design</searchLink>. Oct2015, Vol. 47 Issue 2, p204-229. 26p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Computer+software+termination%22">Computer software termination</searchLink><br /><searchLink fieldCode="DE" term="%22Electronic+data+processing%22">Electronic data processing</searchLink><br /><searchLink fieldCode="DE" term="%22Systems+design%22">Systems design</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+science%22">Computer science</searchLink><br /><searchLink fieldCode="DE" term="%22System+analysis%22">System analysis</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: Two programs are said to be mutually terminating if they terminate on exactly the same inputs. We suggest inference rules and a proof system for proving mutual termination of a given pair of procedures $$\langle $$ $$f$$ , $$f'$$ $$\rangle $$ and the respective subprograms that they call under a free context. Given a (possibly partial) mapping between the procedures of the two programs, the premise of the rule requires proving that given the same arbitrary input in, f( in) and $$f'(in)$$ call procedures mapped in the mapping with the same arguments. A variant of this proof rule with a weaker premise allows to prove termination of one of the programs if the other is known to terminate. In addition, we suggest various techniques for battling the inherent incompleteness of our solution, including a case in which the interface of the two procedures is not identical, and a case in which partial equivalence (the equivalence of their input/output behavior) has only been proven for some, but not all, the outputs of the two given procedures. We present an algorithm for decomposing the verification problem of whole programs to that of proving mutual termination of individual procedures, based on our suggested inference rules. The reported prototype implementation of this algorithm is the first to deal with the mutual termination problem. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Formal Methods in System Design is the property of Springer Nature 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=109575817 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10703-015-0234-3 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 26 StartPage: 204 Subjects: – SubjectFull: Computer software termination Type: general – SubjectFull: Electronic data processing Type: general – SubjectFull: Systems design Type: general – SubjectFull: Computer science Type: general – SubjectFull: System analysis Type: general Titles: – TitleFull: Proving mutual termination. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Elenbogen, Dima – PersonEntity: Name: NameFull: Katz, Shmuel – PersonEntity: Name: NameFull: Strichman, Ofer IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 10 Text: Oct2015 Type: published Y: 2015 Identifiers: – Type: issn-print Value: 09259856 Numbering: – Type: volume Value: 47 – Type: issue Value: 2 Titles: – TitleFull: Formal Methods in System Design Type: main |
| ResultId | 1 |
