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. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., & Yang, H. (2008). Ranking abstractions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4960 LNCS, pp. 148–162). Springer Verlag. https://doi.org/10.1007/978-3-540-78739-6_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
