Ton Chanh Le
Skip Abstract Section
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.
- M. F. Atig, A. Bouajjani, M. Emmi, and A. Lal. Detecting Fair Nontermination in Multithreaded Programs. In CAV, 2012. Google Scholar
Digital Library
- J. Berdine, B. Cook, D. Distefano, and P. W. O’Hearn. Automatic Termination Proofs for Programs with Shape-Shifting Heaps. In CAV, 2006. Google ScholarDigital Library
- J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. W. O’Hearn. Variance analyses from invariance analyses. In POPL, 2007. Google ScholarDigital Library
- M. Bozga, R. Iosif, and F. Koneˇcný. Deciding Conditional Termination. In TACAS, 2012. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. The Polyranking Principle. In ICALP, 2005. Google ScholarDigital Library
- M. Brockschmidt, T. Ströder, C. Otto, and J. Giesl. Automated Detection of Non-Termination and NullPointerExceptions for Java Bytecode. In FoVeOOS, 2011. Google ScholarDigital Library
- M. Brockschmidt, B. Cook, and C. Fuhs. Better termination proving through cooperation. In CAV, 2013. Google ScholarDigital Library
- H.-Y. Chen, B. Cook, C. Fuhs, K. Nimkar, and P. O’Hearn. Proving nontermination via safety. In TACAS, 2014.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- M. Codish, S. Genaim, M. Bruynooghe, J. Gallagher, and W. Vanhoof. One loop at a time. In Intl. Workshop on Termination (WST), 2003.Google Scholar
- B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In SAS, 2005. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI, 2006. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Proving thread termination. In PLDI, 2007. Google ScholarDigital Library
- B. Cook, S. Gulwani, T. Lev-Ami, A. Rybalchenko, and M. Sagiv. Proving conditional termination. In CAV, 2008. Google ScholarDigital Library
- B. Cook, D. Kroening, P. Rümmer, and C. M. Wintersteiger. Ranking Function Synthesis for Bit-Vector Relations. In TACAS, 2010. Google ScholarDigital Library
- B. Cook, A. See, and F. Zuleger. Ramsey vs. Lexicographic Termination Proving. In TACAS, 2013. Google ScholarDigital Library
- P. Cousot. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In VMCAI, 2005. Google ScholarDigital Library
- S. Falke, D. Kapur, and C. Sinz. Termination Analysis of C Programs Using Compiler Intermediate Languages. In RTA, 2011.Google Scholar
- P. Ganty and S. Genaim. Proving termination starting from the end. In CAV, 2013. Google ScholarDigital Library
- C. Gherghina, C. David, S. Qin, and W.-N. Chin. Structured specifications for better verification of heap-manipulating programs. In FM, 2011. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, 2012. Google ScholarDigital Library
- S. Gulwani, S. Srivastava, and R. Venkatesan. Program Analysis As Constraint Solving. In PLDI, 2008. Google ScholarDigital Library
- A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R.-G. Xu. Proving non-termination. In POPL, 2008. Google ScholarDigital Library
- W. R. Harris, A. Lal, A. V. Nori, and S. K. Rajamani. Alternation for Termination. In SAS, 2010. Google ScholarDigital Library
- M. Heizmann, J. Hoenicke, and A. Podelski. Termination Analysis by Learning Terminating Programs. In CAV, 2014. Google ScholarDigital Library
- M. Heizmann, D. Dietsch, J. Leike, B. Musa, and A. Podelski. Ultimate Automizer with Array Interpolation (Competition Contribution). In TACAS, 2015.Google Scholar
- D. Jovanovic and L. M. de Moura. Solving non-linear arithmetic. In IJCAR, 2012. Google ScholarDigital Library
- D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination Analysis with Compositional Transition Invariants. In CAV, 2010. Google ScholarDigital Library
- D. Larraz, A. Oliveras, E. Rodriguez-Carbonell, and A. Rubio. Proving termination of imperative programs using Max-SMT. In FMCAD, 2013.Google ScholarCross Ref
- D. Larraz, K. Nimkar, A. Oliveras, E. Rodriguez-Carbonell, and A. Rubio. Proving Non-termination Using Max-SMT. In CAV, 2014. Google ScholarDigital Library
- Q. L. Le, C. Gherghina, S. Qin, and W.-N. Chin. Shape Analysis via Second-Order Bi-Abduction. In CAV, 2014. Google ScholarDigital Library
- T. C. Le, C. Gherghina, A. Hobor, and W.-N. Chin. A resource-based logic for termination and non-termination proofs. In ICFEM, 2014.Google ScholarCross Ref
- C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In POPL, 2001. Google ScholarDigital Library
- É. Payet and F. Spoto. Experiments with Non-Termination Analysis for Java Bytecode. Electr. Notes Theor. Comput. Sci., 253(5), 2009. Google ScholarDigital Library
- C. S. Peirce. Collected papers of Charles Sanders Peirce. Harvard University Press., 1958.Google Scholar
- A. Podelski and A. Rybalchenko. Transition Invariants. In LICS, 2004. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. A Complete Method for the Synthesis of Linear Ranking Functions. In VMCAI, 2004.Google ScholarCross Ref
- A. Podelski and A. Rybalchenko. ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In PADL, 2007. Google ScholarDigital Library
- C. Popeea and W.-N. Chin. Inferring Disjunctive Postconditions. In ASIAN, 2006. Google ScholarDigital Library
- J. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS, 2002. Google ScholarDigital Library
- A. Rybalchenko. Constraint Solving for Program Verification: Theory and Practice by Example. In CAV, 2010. Google ScholarDigital Library
- A. Schrijver. Theory of Linear and Integer Programming. John Wiley & Sons, New York, 1986. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- SV-COMP. The Competition on Software Verification. http://sv-comp. sosy-lab.org/2015/, 2015.Google Scholar
- TermCOMP. The Annual International Termination Competition. http://termination-portal.org/wiki/Termination_Competition_ 2014/, 2014.Google Scholar
- H. Velroyen and P. Rümmer. Non-termination checking for imperative programs. In TAP, 2008. Google ScholarDigital Library
Index Terms
- Termination and non-termination specification inference
Recommendations
Termination and non-termination specification inference
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationTechniques 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 ...
Innermost termination of context-sensitive rewriting
DLT'02: Proceedings of the 6th international conference on Developments in language theoryContext-sensitive rewriting is a restriction of term rewriting used to model evaluation strategies in functional programming and in programming languages like OBJ. For example, under certain conditions termination of an OBJ program is equivalent to ...
Comments