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.
|
|
| 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] |
|---|---|
| DOI: | 10.1109/ICSE48619.2023.00115 |
