Proving non-termination

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: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 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.
• 5: Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001 [doi>10.1023/A:1011276507260]
• 6: Michael Colón , Henny Sipma, Practical Methods for Proving Program Termination, Proceedings of the 14th International Conference on Computer Aided Verification, p.442-454, July 27-31, 2002
• 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.
• 9: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 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.
• 11: M. d'Amorim and G. Rosu. Efficient monitoring of omega-languages. In Proc. CAV, LNCS 3576, pages 364--378. Springer, 2005.
• 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.
• 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: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 15: Bhargav S. Gulavani , Thomas A. Henzinger , Yamini Kannan , Aditya V. Nori , Sriram K. Rajamani, SYNERGY: a new algorithm for property checking, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181790]
• 16: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 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.
• 20: A. Pnueli, A. Zaks, and L.D. Zuck. Monitoring interfaces for faults. Electr. Notes Theor. Comput. Sci., 144(4): 73--89, 2006.
• 21: Sriram Sankaranarayanan , Henny B. Sipma , Zohar Manna, Non-linear loop invariant generation using Gröbner bases, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.318-329, January 14-16, 2004, Venice, Italy
• 22: Alexander Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
• 23: Koushik Sen , Abhay Vardhan , Gul Agha , Grigore Rosu, Efficient Decentralized Monitoring of Safety in Distributed Systems, Proceedings of the 26th International Conference on Software Engineering, p.418-427, May 23-28, 2004
• 24: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 25: H. Velroyen. Automatic non-termination analysis of imperative programs. Master's thesis, Chalmers University of Technology, Aachen Technical University, 2007.
• 26: Emmett Jethro Witchel , Krste Asanovic, Mondriaan memory protection, Massachusetts Institute of Technology, 2004
• 27: Emmett Witchel , Josh Cates , Krste Asanović, Mondrian memory protection, Proceedings of the 10th international conference on Architectural support for programming languages and operating systems, October 05-09, 2002, San Jose, California
• 28: Emmett Witchel , Junghwan Rhee , Krste Asanović, Mondrix: memory isolation for linux using mondriaan memory protection, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom
• 29: Y. Xie and A. Aiken. Saturn: A SAT-based tool for bug detection. In Proc. CAV, LNCS 3576, pages 139--143. Springer, 2005.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Reliability, Verification

Keywords:
model checking, non-termination, program verification, recurrent sets, testing