--- _id: '4521' abstract: - lang: eng text: The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools.While this is well-understood in safety verification, the current focus of liveness verification has been almost exclusively on the search for termination proofs. A counterexample to termination is an infinite programexecution. In this paper, we propose a method to search for such counterexamples. The search proceeds in two phases. We first dynamically enumerate lasso-shaped candidate paths for counterexamples, and then statically prove their feasibility. We illustrate the utility of our nontermination prover, called TNT, on several nontrivial examples, some of which require bit-level reasoning about integer representations. author: - first_name: Ashutosh full_name: Ashutosh Gupta id: 335E5684-F248-11E8-B48F-1D18A9856A87 last_name: Gupta - first_name: Thomas A full_name: Thomas Henzinger id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Ritankar full_name: Majumdar, Ritankar S last_name: Majumdar - first_name: Andrey full_name: Rybalchenko, Andrey last_name: Rybalchenko - first_name: Ru full_name: Xu, Ru-Gang last_name: Xu citation: ama: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. Proving non-termination. In: ACM; 2008:147-158. doi:10.1145/1328438.1328459' apa: 'Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., & Xu, R. (2008). Proving non-termination (pp. 147–158). Presented at the POPL: Principles of Programming Languages, ACM. https://doi.org/10.1145/1328438.1328459' chicago: Gupta, Ashutosh, Thomas A Henzinger, Ritankar Majumdar, Andrey Rybalchenko, and Ru Xu. “Proving Non-Termination,” 147–58. ACM, 2008. https://doi.org/10.1145/1328438.1328459. ieee: 'A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu, “Proving non-termination,” presented at the POPL: Principles of Programming Languages, 2008, pp. 147–158.' ista: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination. POPL: Principles of Programming Languages, 147–158.' mla: Gupta, Ashutosh, et al. Proving Non-Termination. ACM, 2008, pp. 147–58, doi:10.1145/1328438.1328459. short: A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008, pp. 147–158. conference: name: 'POPL: Principles of Programming Languages' date_created: 2018-12-11T12:09:17Z date_published: 2008-01-01T00:00:00Z date_updated: 2021-01-12T07:59:25Z day: '01' doi: 10.1145/1328438.1328459 extern: 1 main_file_link: - open_access: '0' url: http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf month: '01' page: 147 - 158 publication_status: published publisher: ACM publist_id: '208' quality_controlled: 0 status: public title: Proving non-termination type: conference year: '2008' ...