Exploiting sparsity in difference-bound matrices

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

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

12 Citations (Scopus)

Abstract

Relational numeric abstract domains are very important in program analysis. Common domains, such as Zones and Octagons, are usually conceptualised with weighted digraphs and implemented using difference-bound matrices (DBMs). Unfortunately, though conceptually simple, direct implementations of graph-based domains tend to perform poorly in practice, and are impractical for analyzing large code-bases. We propose new DBM algorithms that exploit sparsity and closed operands. In particular, a new representation which we call split normal form reduces graph density on typical abstract states. We compare the result- ing implementation with several existing DBM-based abstract domains, and show that we can substantially reduce the time to perform full DBM analysis, without sacrificing precision.

Original languageEnglish
Title of host publicationStatic Analysis
Subtitle of host publication23rd International Symposium, SAS 2016 Edinburgh, UK, September 8–10, 2016 Proceedings
EditorsXavier Rival
Place of PublicationBerlin Germany
PublisherSpringer
Pages189-211
Number of pages23
ISBN (Electronic)9783662534137
ISBN (Print)9783662534120
DOIs
Publication statusPublished - 2016
Externally publishedYes
EventStatic Analysis Symposium 2016 - Edinburgh, United Kingdom
Duration: 8 Sep 201610 Sep 2016
Conference number: 23rd
http://staticanalysis.org/sas2016/
https://link.springer.com/book/10.1007/978-3-662-53413-7 (Proceedings)

Publication series

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

Conference

ConferenceStatic Analysis Symposium 2016
Abbreviated titleSAS 2016
CountryUnited Kingdom
CityEdinburgh
Period8/09/1610/09/16
Internet address

Cite this