Disjunctive interval analysis

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

4 Citations (Scopus)

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 interval analysis.

Original languageEnglish
Title of host publication28th International Symposium, SAS 2021 Chicago, IL, USA, October 17–19, 2021 Proceedings
EditorsCezara Drăgoi, Suvam Mukherjee, Kedar Namjoshi
Place of PublicationCham Switzerland
PublisherSpringer
Pages144-165
Number of pages22
ISBN (Electronic)9783030888060
ISBN (Print)9783030888053
DOIs
Publication statusPublished - 2021
EventInternational Symposium on Static Analysis 2021 - Chicago, United States of America
Duration: 17 Oct 202119 Oct 2021
Conference number: 28th
https://link.springer.com/book/10.1007/978-3-030-88806-0 (Proceedings)

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12913
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Symposium on Static Analysis 2021
Abbreviated titleSAS 2021
Country/TerritoryUnited States of America
CityChicago
Period17/10/2119/10/21
Internet address

Keywords

  • Abstract interpretation
  • Boxes
  • Decision diagrams
  • Integer abstract domains

Cite this