More Web Proxy on the site http://driver.im/

research-article

Proving non-termination

Authors:

Ashutosh Gupta,

Thomas A. Henzinger,

Rupak Majumdar,

Andrey Rybalchenko,

Ru-Gang XuAuthors Info & Claims

ACM SIGPLAN Notices, Volume 43, Issue 1

Pages 147 - 158

https://doi.org/10.1145/1328897.1328459

Published: 07 January 2008 Publication History

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.

References

[1]

A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.

Digital Library

[2]

T. Ball and S.K. Rajamani. The Slam project: Debugging system software via static analysis. In Proc. POPL, pages 1--3. ACM, 2002.

Digital Library

[3]

Joshua Bloch. Nearly all binary searches and mergesorts are broken, June 2006. http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html.

[4]

A. Bradley, Z. Manna, and H. Sipma. The polyranking principle. In Proc. ICALP, LNCS 3580, pages 1349--1361. Springer, 2005.

Digital Library

[5]

E.M. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19 (1): 7--34, 2001.

Digital Library

[6]

M. Colon and H. Sipma. Practical methods for proving program termination. In Proc. CAV, LNCS 2404, pages 442--454. Springer, 2002.

Digital Library

[7]

M. Colon, S. Sankaranarayanan, and H.B. Sipma. Linear invariant generation using non-linear constraint solving. In Proc. CAV, LNCS~2725, pages 420--432. Springer, 2003.

[8]

B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In Proc. CAV, LNCS~3576, pages 296--300. Springer, 2005.

Digital Library

[9]

B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In Proc. PLDI, pages 415--426. ACM, 2006.

Digital Library

[10]

P. Cousot. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In Proc. VMCAI, LNCS 3385, pages 1--24. Springer, 2005.

Digital Library

[11]

M. d'Amorim and G. Rosu. Efficient monitoring of omega-languages. In Proc. CAV, LNCS 3576, pages 364--378. Springer, 2005.

Digital Library

[12]

V. Ganesh and D.L. Dill. A decision procedure for bit-vectors and arrays. In Proc. CAV, LNCS 4590, pages 519--531. Springer, 2007.

Digital Library

[13]

P. Godefroid. The soundness of bugs is what matters (position statement). In BUGS'2005 (PLDI'2005 Workshop on the Evaluation of Software Defect Detection Tools), 2005.

[14]

P. Godefroid, N. Klarlund, and K. Sen. Dart: Directed automated random testing. In Proc. PLDI, pages 213--223. ACM, 2005.

Digital Library

[15]

B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, and S.K. Rajamani. Synergy: A new algorithm for property checking. In Proc. FSE, pages 117--127. ACM, 2006.

Digital Library

[16]

T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. POPL, pages 58--70. ACM, 2002.

Digital Library

[17]

C. Holzbaur. OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, 1995. TR-95-09.

[18]

D. Kapur. Automatically generating loop invariants using quantifier elimination. Technical Report 05431 (Deduction and Applications), IBFI Schloss Dagstuhl, 2006.

[19]

T. Kremenek and D.R. Engler. Z-ranking: Using statistical analysis to counter the impact of static analysis approximations. In Proc. SAS, LNCS 2694, pages 295--315. Springer, 2003.

Digital Library

[20]

A. Pnueli, A. Zaks, and L.D. Zuck. Monitoring interfaces for faults. Electr. Notes Theor. Comput. Sci., 144(4): 73--89, 2006.

Digital Library

[21]

S. Sankaranarayanan, H.B. Sipma, and Z. Manna. Non-linear loop invariant generation using Grobner bases. In Proc. POPL, pages 318--329. ACM, 2004.

Digital Library

[22]

A. Schrijver. Theory of Linear and Integer Programming. Wiley, 1986.

Digital Library

[23]

K. Sen, A. Vardhan, G. Agha, and G. Rosu. Efficient decentralized monitoring of safety in distributed systems. In Proc. ICSE, pages 418--427. ACM, 2004.

Digital Library

[24]

K. Sen, D. Marinov, and G. Agha. Cute: A concolic unit testing engine for C. In Proc. ESEC/FSE, pages 263--272. ACM, 2005.

Digital Library

[25]

H. Velroyen. Automatic non-termination analysis of imperative programs. Master's thesis, Chalmers University of Technology, Aachen Technical University, 2007.

[26]

E. Witchel. Mondriaan Memory Protection. PhD thesis, Massachusetts Institute of Technologys, 2004.

Digital Library

[27]

E. Witchel, J. Cates, and K. Asanovic. Mondrian memory protection. In Proc. ASPLOS, pages 304--316. ACM, 2002.

Digital Library

[28]

E. Witchel, J. Rhee, and K. Asanovic. Mondrix: memory isolation for linux using mondriaan memory protection. In Proc. SOSP, pages 31--44. ACM, 2005.

Digital Library

[29]

Y. Xie and A. Aiken. Saturn: A SAT-based tool for bug detection. In Proc. CAV, LNCS 3576, pages 139--143. Springer, 2005.

Digital Library

Cited By

Metta RKarmarkar HMadhukar KVenkatesh RChakraborty S(2024)PROTON: PRObes for Termination Or Not (Competition Contribution)Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57256-2_27(393-398)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57256-2_27
Unno HTerauchi TGu YKoskinen E(2023)Modular Primal-Dual Fixpoint Logic Solving for Temporal VerificationProceedings of the ACM on Programming Languages10.1145/35712657:POPL(2111-2140)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571265
Han ZHe FGrundy JPollock LPenta M(2023)Data-Driven Recurrent Set Learning for Non-termination AnalysisProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00115(1303-1315)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00115
Show More Cited By

Index Terms

Proving non-termination
1. General and reference
  1. Cross-computing tools and techniques
    1. Reliability
2. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging
  2. Software organization and properties
    1. Extra-functional properties
      1. Software reliability

Recommendations

Proving non-termination
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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, ...
Non-termination Proving at Scale

Program termination is a classic non-safety property whose falsification cannot in general be witnessed by a finite trace. This makes testing for non-termination challenging, and also a natural target for symbolic proof. Several works in the literature ...
Proving thread termination
Proceedings of the 2007 PLDI conference

Concurrent programs are often designed such that certain functions executing within critical threads must terminate. Examples of such cases can be found in operating systems, web servers, e-mail clients, etc. Unfortunately, no known automatic program ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 43, Issue 1

POPL '08

January 2008

420 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1328897

Issue’s Table of Contents

POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2008
448 pages
ISBN:9781595936899
DOI:10.1145/1328438
General Chair:
George Necula
University of California, Berkeley
,
Program Chair:
Philip Wadler
University of Edinburgh

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 January 2008

Published in SIGPLAN Volume 43, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

144
Total Citations
View Citations
934
Total Downloads

Downloads (Last 12 months)53
Downloads (Last 6 weeks)8

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Metta RKarmarkar HMadhukar KVenkatesh RChakraborty S(2024)PROTON: PRObes for Termination Or Not (Competition Contribution)Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57256-2_27(393-398)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57256-2_27
Unno HTerauchi TGu YKoskinen E(2023)Modular Primal-Dual Fixpoint Logic Solving for Temporal VerificationProceedings of the ACM on Programming Languages10.1145/35712657:POPL(2111-2140)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571265
Han ZHe FGrundy JPollock LPenta M(2023)Data-Driven Recurrent Set Learning for Non-termination AnalysisProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00115(1303-1315)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00115
Shi XXie XLi YZhang YChen SLi XRoychoudhury ACadar CKim M(2022)Large-scale analysis of non-termination bugs in real-world OSS projectsProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3540250.3549129(256-268)Online publication date: 7-Nov-2022
https://dl.acm.org/doi/10.1145/3540250.3549129
Almagor SChistikov DOuaknine JWorrell J(2022)O-Minimal Invariants for Discrete-Time Dynamical SystemsACM Transactions on Computational Logic10.1145/350129923:2(1-20)Online publication date: 14-Jan-2022
https://dl.acm.org/doi/10.1145/3501299
Stephens JFerles KMariano BLahiri SDillig I(2021)SmartPulse: Automated Checking of Temporal Properties in Smart Contracts2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00085(555-571)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00085
Kura SUnno HHasuo I(2021)Decision Tree Learning in CEGIS-Based Termination AnalysisComputer Aided Verification10.1007/978-3-030-81688-9_4(75-98)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_4
Li YTurrini ASun XZhang L(2020)Proving Non-inclusion of Büchi Automata Based on Monte Carlo SamplingAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_26(467-483)Online publication date: 12-Oct-2020
https://doi.org/10.1007/978-3-030-59152-6_26
Ben-Amram ADoménech JGenaim S(2019)Multiphase-Linear Ranking Functions and Their Relation to Recurrent SetsStatic Analysis10.1007/978-3-030-32304-2_22(459-480)Online publication date: 2-Oct-2019
https://doi.org/10.1007/978-3-030-32304-2_22
David CKesseli PKroening DLewis M(2018)Program Synthesis for Program AnalysisACM Transactions on Programming Languages and Systems10.1145/317480240:2(1-45)Online publication date: 28-May-2018
https://dl.acm.org/doi/10.1145/3174802
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents