Proving program termination

Abstract

In contrast to popular belief, proving termination is not always impossible.

References

1. Babic, D., Hu, A.J., Rakamaric, Z., and Cook, B. Proving termination by divergence. In SEFM, 2007.
2. Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K. and Ustuner, A. Thorough static analysis of device drivers. In Proceedings of EuroSys, 2006.
3. Berdine, J., Chawdhary, A., Cook, B., Distefano, D. and O'Hearn, P. Variance analyses from invariance analyses. In Proceedings of POPL, 2007.
4. Berdine, J., Cook, B., Distefano, D. and O'Hearn, P. Automatic termination proofs for programs with shape-shifting heaps. In Proceedings of CAV, 2006.
5. Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P. and Vojnar, T. Programs with lists are counter automata. In Proceedings of CAV, 2006.
6. Bradley, A., Manna, Z. and Sipma, H. Termination of polynomial programs. In Proceedings of VMCAI, 2005.
7. Bradley, A., Manna, Z. and Sipma, H.B. Linear ranking with reachability. In Proceedings of CAV, 2005.
8. Bradley, A., Manna, Z. and Sipma, H.B. The polyranking principle. In Proceedings of ICALP, 2005.
9. Chawdhary, C., Cook, B., Gulwani, S., Sagiv, M. and Yang, H. Ranking abstractions. In Proceedings of ESOP, 2008.
10. Codish, M., Genaim, S., Bruynooghe, M., Gallagher, J. and Vanhoof, W. One loop at a time. In Proceedings of WST, 2003.
11. Colón, M. and Sipma, H. Synthesis of linear ranking functions. In Proceedings of TACAS, 2001.
12. Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A. and Vardi, M. Proving that programs eventually do something good. In Proceedings of POPL, 2007.
13. Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A. and Sagiv, M. Proving conditional termination. In Proceedings of CAV, 2008.
14. Cook, B., Podelski, A. and Rybalchenko, A. Termination proofs for systems code. In Proceedings of PLDI, 2006.
15. Dershowitz, N., Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. A general framework for automatic termination analysis of logic programs. Appl. Algebra Eng. Commun. Comput., 2001.
16. Farkas, J. Über die Theorie der einfachen Ungleichungen. Journal für die reine und angewandte Mathematik, 1902.
17. Geser, A. Relative termination. PhD dissertation, 1990.
18. Giesl, J., Swiderski, S., Schneider-Kamp, P. and Thiemann, R. Automated termination analysis for Haskell: From term rewriting to programming languages. In Proceedings of RTA, 2006.
19. Giesl, J. Thiemann, R., Schneider-Kamp, P. and Falke, S. Automated termination proofs with AProVE. In Proceedings of RTA, 2004.
20. Gotsman, A., Cook, B., Parkinson, M. and Vafeiadis, V. Proving that non-blocking algorithms don't block. In Proceedings of POPL, 2009.
21. Gupta, A., Henzinger, T., Majumdar, R., Rybalchenko, A., and Xu, R. Proving non-termination. In Proceedings of POPL, 2008.
22. Jones, C.B. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 1983.
23. Jula, H., Tralamazza, D., Zamfir, C. and Candea, G. Deadlock immunity: Enabling systems to defend against deadlocks. In Proceedings of OSDI, 2008.
24. Lee, C.S., Jones, N.D. and Ben-Amram, A.M., The size-change principle for program termination. In Proceedings of POPL, 2001.
25. Magill, S., Berdine, J., Clarke, E. and Cook, B. Arithmetic strengthening for shape analysis. In Proceedings of SAS, 2007.
26. Manolios, P. and Vroon, D. Termination analysis with calling context graphs. In Proceedings of CAV, 2006.
27. McMillan, K.L. Circular compositional reasoning about liveness. In Proceedings of CHARME, 1999.
28. Misra, J and Chandy, K.M. Proofs of networks of processes. IEEE Trans. Software Eng., 1981.
29. Pnueli, A., Podelski, A., and Rybalchenko, A. Separating fairness and well-foundedness for the analysis of fair discrete systems. In Proceedings of TACAS, 2005.
30. Podelski, A, and Rybalchenko, A. A complete method for the synthesis of linear ranking functions. In Proceedings of VMCAI, 2004.
31. Podelski, A, and Rybalchenko, A. Transition invariants. In Proceedings of LICS, 2004.
32. Podelski, A. and Rybalchenko, A. Transition predicate abstraction and fair termination. In Proceedings of POPL, 2005.
33. Podelski, A., Rybalchenko, A., and Wies, T. Heap assumptions on demand. In Proceedings of CAV, 2008.
34. Ramsey, F. On a problem of formal logic. London Math. Soc., 1930.
35. Stix, G. Send in the Terminator. Scientific American (Nov. 2006).
36. Strachey, C. An impossible program. Computer Journal, 1965.
37. Tiwari, A. Termination of linear programs. In Proceedings of CAV, 2004.
38. Turing, A. On computable numbers, with an application to the Entscheidungsproblem. London Mathematical Society, 1936.
39. Turing, A. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, 1949.
40. Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D. and O'Hearn, P. Scalable shape analysis for systems code. In Proceedings of CAV, 2008.

Index Terms

• Computing methodologies

  • Artificial intelligence

    • Knowledge representation and reasoning

  • Symbolic and algebraic manipulation

    • Symbolic and algebraic algorithms

      • Theorem proving algorithms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning

      • Program verification