Skip to main content

Compact Difference Bound Matrices

Chawdhary, Aziem and King, Andy (2017) Compact Difference Bound Matrices. In: Chang, Evan, ed. 15th Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science . Springer, pp. 471-490. ISBN 978-3-319-71236-9. (doi:10.1007/978-3-319-71237-6_23) (KAR id:62853)

Abstract

The Octagon domain, which tracks a restricted class of two variable inequality, is the abstract domain of choice for many applications because its domain operations are either quadratic or cubic in the number of program variables. Octagon constraints are classically represented using a Difference Bound Matrix (DBM), where the entries in the DBM store bounds c for inequalities of the form x_i - x_j <= c, x_i + x_j <= c or -x_i - x_j <= c. The size of such a DBM is quadratic in the number of variables, giving a representation which can be excessively large for number systems such as rationals. This paper proposes a compact representation for DBMs, in which repeated numbers are factored out of the DBM. The paper explains how the entries of a DBM are distributed, and how this distribution can be exploited to save space and significantly speed-up long-running analyses. Moreover, unlike sparse representations, the domain operations retain their conceptually simplicity and ease of implementation whilst reducing memory usage.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-319-71237-6_23
Subjects: Q Science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 16 Aug 2017 11:00 UTC
Last Modified: 09 Dec 2022 03:37 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62853 (The current URI for this page, for reference purposes)

University of Kent Author Information

Chawdhary, Aziem.

Creator's ORCID:
CReDIT Contributor Roles:

King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.