be converted into questions of fair termination—termination proving were certain non-terminating executions are deemed unfair via given fairness constraints, and thus ignored. Current tools, in fact, either perform this reduction, or simply require the user to express liveness constraints directly as the set of fairness constraints. 12, 29 Neither approach is optimal: the reduction from liveness to fairness is inefficient in the size of the conversion, and fairness constraints are difficult for humans to understand when used directly. An avenue for future work would be to directly prove liveness properties, perhaps as an adaption of existing termination proving techniques.

Dynamic analysis and crash dumps for liveness bugs. In this article we have focused only on static, or compile-time, proof techniques rather than techniques for diagnosing divergence during execution. Some effort has been placed into the area of automatically detecting deadlock during execution time. With new developments in the area of program termination proving we might find that automatic methods of discovering livelock could also now be possible. Temporary modifications to scheduling, or other techniques, might also be employed to help programs not diverge even in cases where they do not guarantee termination or other liveness properties. Some preliminary work has begun to emerge in this area (see Jula et al. 23) but more work is needed.

Scalability, performance, and precision. Scalability to large and complex programs is currently a problem for modern termination provers— current techniques are known, at best, to scale to simple systems code of 30,000 lines of code. Another problem we face is one of precision. Some small programs currently cannot be proved terminating with existing tools. Turing’s undecidability result, of course, states that this will always be true, but this does preclude us from improving precision for various classes of programs and concrete examples. The most famous example is that of the Collatz’ problem, which amounts to proving the termination or non-termination of the program in Figure 11. Currently no proof of this program’s termination behavior is known.

Conclusion

This article has surveyed recent advances in program termination proving techniques for sequential programs, and pointed toward ongoing work and potential areas for future development. The hope of many tool builders in this area is that the current and future termination proving techniques will become generally available for developers wishing to directly prove termination or liveness. We also hope that termination-related applications—such as detecting livelock at runtime or Wang’s tiling problem— will also benefit from these advances.

acknowledgments

The authors would like to thank Lucas Bourdeaux, Abigail See, Tim Harris, Ralf Herbrich, Peter O’Hearn, and Hongseok Yang for their reading of early drafts of this article and suggestions for improvement.

 

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 WS T, 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. uber 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 R TA, 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. Soft ware 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.

 

Byron Cook is a Principal researcher at Microsoft’s research laboratory at Cambridge university, and a professor of computer science at Queen Mary, university of london, england.

Andreas Podelski is a professor of computer science at the university of Freiburg, Germany.

Andrey Rybalchenko is a professor of computer science at the Technische universität München, Germany.