research-article

Termination and non-termination specification inference

Authors:

Wei-Ngan ChinAuthors Info & Claims

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 489 - 498

https://doi.org/10.1145/2737924.2737993

Published: 03 June 2015 Publication History

Abstract

Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same time. We first introduce the concept of second-order termination constraints and accumulate a set of relational assumptions on them via a Hoare-style verification. We then solve these assumptions with case analysis to determine the (conditional) termination and non- termination scenarios expressed in some specification logic form. In contrast to current approaches, our technique can construct a summary of terminating and non-terminating behaviors for each method. This enables modularity and reuse for our termination and non-termination proving processes. We have tested our tool on sample programs from a recent termination competition, and compared favorably against state-of-the-art termination analyzers.

References

[1]

M. F. Atig, A. Bouajjani, M. Emmi, and A. Lal. Detecting Fair Nontermination in Multithreaded Programs. In CAV, 2012.

Digital Library

[2]

J. Berdine, B. Cook, D. Distefano, and P. W. O’Hearn. Automatic Termination Proofs for Programs with Shape-Shifting Heaps. In CAV, 2006.

Digital Library

[3]

J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W. O’Hearn. Variance analyses from invariance analyses. In POPL, 2007.

Digital Library

[4]

M. Bozga, R. Iosif, and F. Koneˇcný. Deciding Conditional Termination. In TACAS, 2012.

Digital Library

[5]

A. R. Bradley, Z. Manna, and H. B. Sipma. The Polyranking Principle. In ICALP, 2005.

Digital Library

[6]

M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl. Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode. In FoVeOOS, 2011.

Digital Library

[7]

M. Brockschmidt, B. Cook, and C. Fuhs. Better termination proving through cooperation. In CAV, 2013.

Digital Library

[8]

H.-Y. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. O’Hearn. Proving nontermination via safety. In TACAS, 2014.

[9]

W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming, 77(9), 2012.

Digital Library

[10]

M. Codish, S. Genaim, M. Bruynooghe, J. Gallagher, and W. Vanhoof. One loop at a time. In Intl. Workshop on Termination (WST), 2003.

[11]

B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In SAS, 2005.

Digital Library

[12]

B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI, 2006.

Digital Library

[13]

B. Cook, A. Podelski, and A. Rybalchenko. Proving thread termination. In PLDI, 2007.

Digital Library

[14]

B. Cook, S. Gulwani, T. Lev-Ami, A. Rybalchenko, and M. Sagiv. Proving conditional termination. In CAV, 2008.

Digital Library

[15]

B. Cook, D. Kroening, P. Rümmer, and C. M. Wintersteiger. Ranking Function Synthesis for Bit-Vector Relations. In TACAS, 2010.

Digital Library

[16]

B. Cook, A. See, and F. Zuleger. Ramsey vs. Lexicographic Termination Proving. In TACAS, 2013.

Digital Library

[17]

P. Cousot. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In VMCAI, 2005.

Digital Library

[18]

S. Falke, D. Kapur, and C. Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages. In RTA, 2011.

[19]

P. Ganty and S. Genaim. Proving termination starting from the end. In CAV, 2013.

Digital Library

[20]

C. Gherghina, C. David, S. Qin, and W.-N. Chin. Structured specifications for better verification of heap-manipulating programs. In FM, 2011.

Digital Library

[21]

J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Proving Termination of Programs Automatically with AProVE. In IJCAR, 2014.

[22]

S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, 2012.

Digital Library

[23]

S. Gulwani, S. Srivastava, and R. Venkatesan. Program Analysis As Constraint Solving. In PLDI, 2008.

Digital Library

[24]

A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G. Xu. Proving non-termination. In POPL, 2008.

Digital Library

[25]

W. R. Harris, A. Lal, A. V. Nori, and S. K. Rajamani. Alternation for Termination. In SAS, 2010.

Digital Library

[26]

M. Heizmann, J. Hoenicke, and A. Podelski. Termination Analysis by Learning Terminating Programs. In CAV, 2014.

Digital Library

[27]

M. Heizmann, D. Dietsch, J. Leike, B. Musa, and A. Podelski. Ultimate Automizer with Array Interpolation (Competition Contribution). In TACAS, 2015.

[28]

D. Jovanovic and L. M. de Moura. Solving non-linear arithmetic. In IJCAR, 2012.

Digital Library

[29]

D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination Analysis with Compositional Transition Invariants. In CAV, 2010.

Digital Library

[30]

D. Larraz, A. Oliveras, E. Rodriguez-Carbonell, and A. Rubio. Proving termination of imperative programs using Max-SMT. In FMCAD, 2013.

[31]

D. Larraz, K. Nimkar, A. Oliveras, E. Rodriguez-Carbonell, and A. Rubio. Proving Non-termination Using Max-SMT. In CAV, 2014.

Digital Library

[32]

Q. L. Le, C. Gherghina, S. Qin, and W.-N. Chin. Shape Analysis via Second-Order Bi-Abduction. In CAV, 2014.

Digital Library

[33]

T. C. Le, C. Gherghina, A. Hobor, and W.-N. Chin. A resource-based logic for termination and non-termination proofs. In ICFEM, 2014.

[34]

C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In POPL, 2001.

Digital Library

[35]

É. Payet and F. Spoto. Experiments with Non-Termination Analysis for Java Bytecode. Electr. Notes Theor. Comput. Sci., 253(5), 2009.

Digital Library

[36]

C. S. Peirce. Collected papers of Charles Sanders Peirce. Harvard University Press., 1958.

[37]

A. Podelski and A. Rybalchenko. Transition Invariants. In LICS, 2004.

Digital Library

[38]

A. Podelski and A. Rybalchenko. A Complete Method for the Synthesis of Linear Ranking Functions. In VMCAI, 2004.

[39]

A. Podelski and A. Rybalchenko. ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In PADL, 2007.

Digital Library

[40]

C. Popeea and W.-N. Chin. Inferring Disjunctive Postconditions. In ASIAN, 2006.

Digital Library

[41]

J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS, 2002.

Digital Library

[42]

A. Rybalchenko. Constraint Solving for Program Verification: Theory and Practice by Example. In CAV, 2010.

Digital Library

[43]

A. Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, New York, 1986.

Digital Library

[44]

T. Ströder, C. Aschermann, F. Frohn, J. Hensel, and J. Giesl. AProVE: Termination and Memory Safety of C Programs (Competition Contribution). In TACAS, 2015.

Digital Library

[45]

SV-COMP. The Competition on Software Verification. http://sv-comp. sosy-lab.org/2015/, 2015.

[46]

TermCOMP. The Annual International Termination Competition. http://termination-portal.org/wiki/Termination_Competition_ 2014/, 2014.

[47]

H. Velroyen and P. Rümmer. Non-termination checking for imperative programs. In TAP, 2008.

Digital Library

Cited By

Kafle BGange GSchachte PSøndergaard HStuckey P(2024)A lightweight approach to nontermination inference using Constrained Horn ClausesSoftware and Systems Modeling (SoSyM)10.1007/s10270-024-01161-523:2(319-342)Online publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1007/s10270-024-01161-5
Wen CCao JSu JXu ZQin SHe MLi HCheung STian C(2024)Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program VerificationComputer Aided Verification10.1007/978-3-031-65630-9_16(302-328)Online publication date: 25-Jul-2024
https://doi.org/10.1007/978-3-031-65630-9_16
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

Termination and non-termination specification inference

Recommendations

Termination and non-termination specification inference
PLDI '15

Techniques for proving termination and non-termination of imperative programs are usually considered as orthogonal mechanisms. In this paper, we propose a novel mechanism that analyzes and proves both program termination and non-termination at the same ...
Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems

Yi and Sakai [Y. Wang and M. Sakai. Decidability of termination for semi-constructor trss, left-linear shallow trss and related systems. In the 17th International Conference on Rewriting Techniques and Applications, volume 4098 of Lecture Notes in ...
From Outermost Termination to Innermost Termination
SOFSEM '09: Proceedings of the 35th Conference on Current Trends in Theory and Practice of Computer Science

Rewriting is the underlying evaluation mechanism of functional programming languages. Therefore, termination analysis of term rewrite systems (TRSs) is an important technique for program verification. To capture the evaluation mechanism of a programming ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2015

630 pages

ISBN:9781450334686

DOI:10.1145/2737924

General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

ACM SIGPLAN Notices Volume 50, Issue 6
PLDI '15
June 2015
630 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2813885
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 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 the author(s) 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].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 June 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Ministry of Education - Singapore

Conference

PLDI '15

Sponsor:

SIGPLAN

PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 13 - 17, 2015

OR, Portland, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

43
Total Citations
View Citations
506
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)2

Reflects downloads up to 30 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kafle BGange GSchachte PSøndergaard HStuckey P(2024)A lightweight approach to nontermination inference using Constrained Horn ClausesSoftware and Systems Modeling (SoSyM)10.1007/s10270-024-01161-523:2(319-342)Online publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1007/s10270-024-01161-5
Wen CCao JSu JXu ZQin SHe MLi HCheung STian C(2024)Enchanting Program Specification Synthesis by Large Language Models Using Static Analysis and Program VerificationComputer Aided Verification10.1007/978-3-031-65630-9_16(302-328)Online publication date: 25-Jul-2024
https://doi.org/10.1007/978-3-031-65630-9_16
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
Zhang YXie XLi YChen SZhang CLi X(2023)EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)10.1109/ASE56229.2023.00061(686-697)Online publication date: 11-Sep-2023
https://doi.org/10.1109/ASE56229.2023.00061
Xu RChen JHe FDwyer MDamian DZeller A(2022)Data-driven loop bound learning for termination analysisProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510220(499-510)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510220
Zhu SKincaid ZFreund SYahav E(2021)Termination analysis without the tearsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454110(1296-1311)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454110
Chatterjee KGoharshady ENovotný PŽikelić ĐFreund SYahav E(2021)Proving non-termination by program reversalProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454093(1033-1048)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454093
Kafle BGange GSchachte PSøndergaard HStuckey P(2021)Lightweight Nontermination Inference with CHCsSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_22(383-402)Online publication date: 3-Dec-2021
https://doi.org/10.1007/978-3-030-92124-8_22
Zhu SKincaid Z(2021)Reflections on Termination of Linear LoopsComputer Aided Verification10.1007/978-3-030-81688-9_3(51-74)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_3
He FHan J(2020)Termination analysis for evolving programs: an incremental approach by reusing certified modulesProceedings of the ACM on Programming Languages10.1145/34282674:OOPSLA(1-27)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428267
Show More Cited By

View Options

Get Access

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 Table of Contents