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:https://doi.org/10.1007/978-3-319-71237-6_23) (Full text available)

PDF (Compact Difference Bound Matrices) - Pre-print
Download (320kB) Preview
[img]
Preview
Official URL
http://dx.doi.org/10.1007/978-3-319-71237-6_23

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
Subjects: Q Science
Divisions: Faculties > Sciences > School of Computing
Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Andy King
Date Deposited: 16 Aug 2017 11:00 UTC
Last Modified: 11 Dec 2017 12:29 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/62853 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year