Book Chapter

Disjunctive Interval Analysis

Graeme Gange, Jorge A Navas, Peter Schachte, Harald Sondergaard, Peter J Stuckey

Static Analysis | Lecture Notes in Artificial Intelligence | SPRINGER INTERNATIONAL PUBLISHING AG | Published : 2021

Abstract

We revisit disjunctive interval analysis based on the Boxes abstract domain. We propose the use of what we call range decision diagrams (RDDs) to implement Boxes, and we provide algorithms for the necessary RDD operations. RDDs tend to be more compact than the linear decision diagrams (LDDs) that have traditionally been used for Boxes. Representing information more directly, RDDs also allow for the implementation of more accurate abstract operations. This comes at no cost in terms of analysis efficiency, whether LDDs utilise dynamic variable ordering or not. RDD and LDD implementations are available in the Crab analyzer, and our experiments confirm that RDDs are well suited for disjunctive i..

View full abstract

Grants

Awarded by National Science Foundation


Funding Acknowledgements

We thank the three anonymous reviewers for their careful reading of an earlier version of the paper, and their constructive suggestions for how to improve it. Jorge Navas has been supported by the National Science Foundation under grant number 1816936.