Ashutosh Gupta
Thomas A. Henzinger
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.
- A.V. Aho, R. Sethi, and J.D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986. Google Scholar
Digital Library
- T. Ball and S.K. Rajamani. The Slam project: Debugging system software via static analysis. In Proc. POPL, pages 1--3. ACM, 2002. Google ScholarDigital Library
- 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.Google Scholar
- A. Bradley, Z. Manna, and H. Sipma. The polyranking principle. In Proc. ICALP, LNCS 3580, pages 1349--1361. Springer, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. Colon and H. Sipma. Practical methods for proving program termination. In Proc. CAV, LNCS 2404, pages 442--454. Springer, 2002. Google ScholarDigital Library
- 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.Google Scholar
- B. Cook, D. Kroening, and N. Sharygina. Cogent: Accurate theorem proving for program verification. In Proc. CAV, LNCS~3576, pages 296--300. Springer, 2005. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In Proc. PLDI, pages 415--426. ACM, 2006. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. d'Amorim and G. Rosu. Efficient monitoring of omega-languages. In Proc. CAV, LNCS 3576, pages 364--378. Springer, 2005. Google ScholarDigital Library
- V. Ganesh and D.L. Dill. A decision procedure for bit-vectors and arrays. In Proc. CAV, LNCS 4590, pages 519--531. Springer, 2007. Google ScholarDigital Library
- 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.Google Scholar
- P. Godefroid, N. Klarlund, and K. Sen. Dart: Directed automated random testing. In Proc. PLDI, pages 213--223. ACM, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. POPL, pages 58--70. ACM, 2002. Google ScholarDigital Library
- C. Holzbaur. OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, 1995. TR-95-09.Google Scholar
- D. Kapur. Automatically generating loop invariants using quantifier elimination. Technical Report 05431 (Deduction and Applications), IBFI Schloss Dagstuhl, 2006.Google Scholar
- 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. Google ScholarDigital Library
- A. Pnueli, A. Zaks, and L.D. Zuck. Monitoring interfaces for faults. Electr. Notes Theor. Comput. Sci., 144(4): 73--89, 2006. Google ScholarDigital Library
- S. Sankaranarayanan, H.B. Sipma, and Z. Manna. Non-linear loop invariant generation using Grobner bases. In Proc. POPL, pages 318--329. ACM, 2004. Google ScholarDigital Library
- A. Schrijver. Theory of Linear and Integer Programming. Wiley, 1986. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- K. Sen, D. Marinov, and G. Agha. Cute: A concolic unit testing engine for C. In Proc. ESEC/FSE, pages 263--272. ACM, 2005. Google ScholarDigital Library
- H. Velroyen. Automatic non-termination analysis of imperative programs. Master's thesis, Chalmers University of Technology, Aachen Technical University, 2007.Google Scholar
- E. Witchel. Mondriaan Memory Protection. PhD thesis, Massachusetts Institute of Technologys, 2004. Google ScholarDigital Library
- E. Witchel, J. Cates, and K. Asanovic. Mondrian memory protection. In Proc. ASPLOS, pages 304--316. ACM, 2002. Google ScholarDigital Library
- E. Witchel, J. Rhee, and K. Asanovic. Mondrix: memory isolation for linux using mondriaan memory protection. In Proc. SOSP, pages 31--44. ACM, 2005. Google ScholarDigital Library
- Y. Xie and A. Aiken. Saturn: A SAT-based tool for bug detection. In Proc. CAV, LNCS 3576, pages 139--143. Springer, 2005. Google ScholarDigital Library
Index Terms
- Proving non-termination
Recommendations
Proving non-termination
POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThe 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, ...
Proving thread termination
Proceedings of the 2007 PLDI conferenceConcurrent 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 ...
Formal Verification for C Program
Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The ...
Comments