Abstract
We propose an abstract interpretation algorithm for proving that a program terminates on all inputs. The algorithm uses a novel abstract domain which uses ranking relations to conservatively represent relations between intermediate program states. One of the attractive aspects of the algorithm is that it abstracts information that is usually not important for proving termination such as program invariants and yet it distinguishes between different reasons for termination which are not usually maintained in existing abstract domains. We have implemented a prototype of the algorithm and shown that in practice it is fast and precise.
Chapter PDF
Similar content being viewed by others
Keywords
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
Balaban, I., Pnueli, A., Zuck, L.: Ranking abstraction as companion to predicate abstraction. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, Springer, Heidelberg (2005)
Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O’Hearn, P.: Variance analyses from invariance analyses. In: POPL 2007 (2007)
Bradley, A., Manna, Z., Sipma, H.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, Springer, Heidelberg (2005)
Bruynooghe, M., Codish, M., Gallagher, J., Genaim, S., Vanhoof, W.: Termination analysis through combination of type based norms. ACM Trans. Progam. Lang. Syst. 29(2) (2007)
Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H.: Ranking abstractions. Manuscript (2008), http://www.dcs.qmul.ac.uk/~aiem/paper/esop08-full.pdf
Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming 41(1) (1999)
Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006 (2006)
Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, Springer, Heidelberg (2006)
Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Comput. Sci. 277(1–2), 47–103 (2002)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979 (1979)
Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking (2003)
Jeannet, B.: NewPolka polyhedra library, http://pop-art.inrialpes.fr/people/bjeannet/newpolka/index.html
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL 2001 (2001)
Miné, A.: The Octagon abstract domain. Higher-Order and Symbolic Comput. 19, 31–100 (2006)
Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, Springer, Heidelberg (2002)
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, Springer, Heidelberg (2004)
Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004 (2004)
Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67–69 (1948), Reprinted In: The early British computer conferences. Charles Babbage Institute Reprint Series for the History of Computing, vol. 14, MIT Press, Cambridge (1989)
Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. Logic Journal of IGPL (September 2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H. (2008). Ranking Abstractions. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)