Advertisement

Proving Non-termination Using Max-SMT

  • Daniel Larraz
  • Kaustubh Nimkar
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Albert Rubio
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

We show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants – properties such that if they hold at a location during execution once, then they will continue to hold at that location from then onwards. The check that quasi-invariants can indeed be reached is then performed separately. Our technique considers strongly connected subgraphs of a program’s control flow graph for analysis and thus produces more generic witnesses of non-termination than existing methods. Moreover, it can handle programs with unbounded non-determinism and is more likely to converge than previous approaches.

Keywords

Transition Relation Soft Constraint Hard Constraint Program Variable Invariant Generation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Francez, N., Grumberg, O., Katz, S., Pnueli, A.: Proving Termination of Prolog Programs. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 89–105. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  2. 2.
    Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advances in Verification, pp. 1–8 (2000)Google Scholar
  3. 3.
    Colón, M. A., Sipma, H. B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 113–129. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349–1361. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491–504. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Bradley, A.R., Manna, Z., Sipma, H.B.: Termination analysis of integer linear loops. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 488–502. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proc. PLDI 2006, pp. 415–426. ACM Press (2006)Google Scholar
  11. 11.
    Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Babic, D., Hu, A.J., Rakamaric, Z., Cook, B.: Proving termination by divergence. In: SEFM, pp. 93–102. IEEE Computer Society (2007)Google Scholar
  14. 14.
    Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 328–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: No return! Formal Methods in System Design 35(3), 369–387 (2009)CrossRefzbMATHGoogle Scholar
  16. 16.
    Otto, C., Brockschmidt, M., Essen, C.V., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proc. RTA 2010. LIPIcs, vol. 6, pp. 259–276. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Edinburgh (2010)Google Scholar
  17. 17.
    Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 89–103. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  18. 18.
    Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 81–95. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  19. 19.
    Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413–429. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  20. 20.
    Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 47–61. Springer, Heidelberg (2013)Google Scholar
  21. 21.
    Babic, D., Cook, B., Hu, A.J., Rakamaric, Z.: Proving termination of nonlinear command sequences. Formal Asp. Comput. 25(3), 389–403 (2013)CrossRefMathSciNetGoogle Scholar
  22. 22.
    Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. Formal Methods in System Design 43(1), 93–120 (2013)CrossRefGoogle Scholar
  23. 23.
    Larraz, D., Rodríguez-Carbonell, E., Rubio, A.: Smt-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169–188. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  24. 24.
    Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving Termination of Imperative Programs Using Max-SMT. In: Proc. FMCAD 2013 (2013)Google Scholar
  25. 25.
    Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  26. 26.
    Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (February 2009)Google Scholar
  27. 27.
    Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  28. 28.
    Schrijver, A.: Theory of Linear and Integer Programming. Wiley (June 1998)Google Scholar
  29. 29.
    Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions (submitted, 2014)Google Scholar
  30. 30.
    Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  31. 31.
    Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.: Proving nontermination via safety. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156–171. Springer, Heidelberg (2014)Google Scholar
  32. 32.
    Spoto, F., Mesnard, F., Payet, É.: A termination analyzer for Java bytecode based on path-length. ACM TOPLAS 32(3) (2010)Google Scholar
  33. 33.
    Payet, É., Spoto, F.: Experiments with Non-Termination Analysis for Java Bytecode. Electr. Notes Theor. Comput. Sci. 253(5), 83–96 (2009)CrossRefGoogle Scholar
  34. 34.
    Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 123–141. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  35. 35.
    Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving non-termination. In: Necula, G.C., Wadler, P. (eds.) Proc. POPL 2008, pp. 147–158. ACM Press (2008)Google Scholar
  36. 36.
    de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  37. 37.
    Velroyen, H., Rümmer, P.: Non-termination checking for imperative programs. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 154–170. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  38. 38.
    Petit, J., Giménez, O., Roura, S.: Jutge.org: An educational programming judge. In: King, L.A.S., Musicant, D.R., Camp, T., Tymann, P.T. (eds.) SIGCSE, pp. 445–450. ACM (2012)Google Scholar
  39. 39.
    Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Gupta, R., Amarasinghe, S.P. (eds.) Proc. PLDI 2008, pp. 281–292. ACM Press (2008)Google Scholar
  40. 40.
    Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 304–319. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  41. 41.
    Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 415–418. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  42. 42.
    Atig, M.F., Bouajjani, A., Emmi, M., Lal, A.: Detecting fair non-termination in multithreaded programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 210–226. Springer, Heidelberg (2012)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Daniel Larraz
    • 1
  • Kaustubh Nimkar
    • 2
  • Albert Oliveras
    • 1
  • Enric Rodríguez-Carbonell
    • 1
  • Albert Rubio
    • 1
  1. 1.Universitat Politècnica de CatalunyaBarcelonaSpain
  2. 2.University College LondonUnited Kingdom

Personalised recommendations