Data-Driven Recurrent Set Learning for Non-termination Analysis.
Saved in:
| Title: | Data-Driven Recurrent Set Learning for Non-termination Analysis. |
|---|---|
| Authors: | Han, Zhilei1 hzl21@mails.tsinghua.edu.cn, He, Fei1 hefei@tsinghua.edu.cn |
| Source: | ICSE: International Conference on Software Engineering. 2023, p1303-1315. 13p. |
| Subjects: | Program termination (Education), Algorithms, Benchmarking (Management), Evaluation, Evaluation research |
| Abstract: | Termination is a fundamental liveness property for program verification. In this paper, we revisit the problem of non-termination analysis and propose the first data-driven learning algorithm for synthesizing recurrent sets, where the non-terminating samples are effectively speculated by a novel method. To ensure convergence of learning, we develop a learning algorithm which is guaranteed to converge to a valid recurrent set if one exists, and thus establish its relative completeness. The methods are implemented in a prototype tool, and experimental results on public benchmarks show its efficacy in proving non-termination as it outperforms state-of-the-art tools, both in terms of cases solved and performance. Evaluation on nonlinear programs also demonstrates its ability to handle complex programs. [ABSTRACT FROM AUTHOR] |
| Copyright of ICSE: International Conference on Software Engineering 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 |
|
Full text is not displayed to guests.
Login for full access.
|
|
| FullText | Links: – Type: pdflink Text: Availability: 1 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 185196085 AccessLevel: 6 PubType: Conference PubTypeId: conference PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Data-Driven Recurrent Set Learning for Non-termination Analysis. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Han%2C+Zhilei%22">Han, Zhilei</searchLink><relatesTo>1</relatesTo><i> hzl21@mails.tsinghua.edu.cn</i><br /><searchLink fieldCode="AR" term="%22He%2C+Fei%22">He, Fei</searchLink><relatesTo>1</relatesTo><i> hefei@tsinghua.edu.cn</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22ICSE%3A+International+Conference+on+Software+Engineering%22">ICSE: International Conference on Software Engineering</searchLink>. 2023, p1303-1315. 13p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Program+termination+%28Education%29%22">Program termination (Education)</searchLink><br /><searchLink fieldCode="DE" term="%22Algorithms%22">Algorithms</searchLink><br /><searchLink fieldCode="DE" term="%22Benchmarking+%28Management%29%22">Benchmarking (Management)</searchLink><br /><searchLink fieldCode="DE" term="%22Evaluation%22">Evaluation</searchLink><br /><searchLink fieldCode="DE" term="%22Evaluation+research%22">Evaluation research</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: Termination is a fundamental liveness property for program verification. In this paper, we revisit the problem of non-termination analysis and propose the first data-driven learning algorithm for synthesizing recurrent sets, where the non-terminating samples are effectively speculated by a novel method. To ensure convergence of learning, we develop a learning algorithm which is guaranteed to converge to a valid recurrent set if one exists, and thus establish its relative completeness. The methods are implemented in a prototype tool, and experimental results on public benchmarks show its efficacy in proving non-termination as it outperforms state-of-the-art tools, both in terms of cases solved and performance. Evaluation on nonlinear programs also demonstrates its ability to handle complex programs. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of ICSE: International Conference on Software Engineering 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=185196085 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1109/ICSE48619.2023.00115 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 13 StartPage: 1303 Subjects: – SubjectFull: Program termination (Education) Type: general – SubjectFull: Algorithms Type: general – SubjectFull: Benchmarking (Management) Type: general – SubjectFull: Evaluation Type: general – SubjectFull: Evaluation research Type: general Titles: – TitleFull: Data-Driven Recurrent Set Learning for Non-termination Analysis. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Han, Zhilei – PersonEntity: Name: NameFull: He, Fei IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 05 Text: 2023 Type: published Y: 2023 Titles: – TitleFull: ICSE: International Conference on Software Engineering Type: main |
| ResultId | 1 |
