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. 471490. ISBN 9783319712369. (doi:10.1007/9783319712376_23)
PDF (Compact Difference Bound Matrices)  Preprint  
Download (320kB)
Preview



Official URL http://dx.doi.org/10.1007/9783319712376_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 speedup longrunning 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/9783319712376_23 
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:  29 May 2019 19:22 UTC 
Resource URI:  https://kar.kent.ac.uk/id/eprint/62853 (The current URI for this page, for reference purposes) 
 Export to:
 RefWorks
 EPrints3 XML
 BibTeX
 CSV
 Depositors only (login required):