Skip to Main content Skip to Navigation
Conference papers

The Abstract Domain of Segmented Ranking Functions

Caterina Urban 1, 2, *
* Corresponding author
1 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
2 Abstraction
LIENS - Laboratoire d'informatique de l'école normale supérieure
Abstract : We present a parameterized abstract domain for proving program termination by abstract interpretation. The domain automatically synthesizes piecewise-defined ranking functions and infers sufficient conditions for program termination. The analysis uses over-approximations but we prove its soundness, meaning that all program executions respecting these sufficient conditions are indeed terminating. The abstract domain is parameterized by a numerical abstract domain for environments and a numerical abstract domain for functions. This parameterization allows to easily tune the trade-off between precision and cost of the analysis. We describe an instantiation of this generic do- main with intervals and affine functions. We define all abstract operators, including widening to ensure convergence. To illustrate the potential of the proposed framework, we have implemented a research prototype static analyzer, for a small imperative language, that yielded interesting preliminary results.
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download
Contributor : Antoine Miné <>
Submitted on : Wednesday, January 8, 2014 - 2:05:08 PM
Last modification on : Tuesday, September 22, 2020 - 3:46:48 AM
Long-term archiving on: : Tuesday, April 8, 2014 - 10:57:36 PM


Files produced by the author(s)




Caterina Urban. The Abstract Domain of Segmented Ranking Functions. Static Analysis, 20th International Symposium,, Jun 2013, Seattle, United States. pp.43-62, ⟨10.1007/978-3-642-38856-9_5⟩. ⟨hal-00925670⟩



Record views


Files downloads