--- res: bibo_abstract: - 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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Ashutosh foaf_name: Ashutosh Gupta foaf_surname: Gupta foaf_workInfoHomepage: http://www.librecat.org/personId=335E5684-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Thomas A foaf_name: Thomas Henzinger foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Ritankar foaf_name: Majumdar, Ritankar S foaf_surname: Majumdar - foaf_Person: foaf_givenName: Andrey foaf_name: Rybalchenko, Andrey foaf_surname: Rybalchenko - foaf_Person: foaf_givenName: Ru foaf_name: Xu, Ru-Gang foaf_surname: Xu bibo_doi: 10.1145/1328438.1328459 dct_date: 2008^xs_gYear dct_publisher: ACM@ dct_title: Proving non-termination@ ...