Paper Info
Title
A Decision Tree Abstract Domain for Proving Conditional Termination.
Abstract
We present a new parameterized abstract domain able to refine existing numerical abstract domains with finite disjunctions. The elements of the abstract domain are decision trees where the decision nodes are labeled with linear constraints, and the leaf nodes belong to a numerical abstract domain. The abstract domain is parametric in the choice between the expressivity and the cost of the linear constraints for the decision nodes (e.g., polyhedral or octagonal constraints), and the choice of the abstract domain for the leaf nodes. We describe an instance of this domain based on piecewise-defined ranking functions for the automatic inference of sufficient preconditions for program termination. We have implemented a static analyzer for proving conditional termination of programs written in (a subset of) C and, using experimental evidence, we show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art and is able to analyze programs that are out of the reach of existing methods.
Year
DOI
Venue
2014
10.1007/978-3-319-10936-7_19
Lecture Notes in Computer Science
Field
DocType
Volume
Decision tree,Parameterized complexity,Computer science,Tree (data structure),Algorithm,Theoretical computer science
Conference
8723
ISSN
Citations 
PageRank 
0302-9743
21
0.72
References 
Authors
27
2
Name
Order
Citations
PageRank
Caterina Urban1795.39
Antoine Miné2111751.15