Name
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 resulting 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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-662-53413-7_10 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Graph,Computer science,Matrix (mathematics),Operand,Theoretical computer science,Implementation,Exploit,Program analysis,dBm,Dense graph | Conference | 9837 |
ISSN | Citations | PageRank |
0302-9743 | 5 | 0.43 |
References | Authors | |
15 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Graeme Gange | 1 | 137 | 24.27 |
| Jorge A. Navas | 2 | 157 | 9.88 |
| Peter Schachte | 3 | 256 | 22.76 |
| Harald Søndergaard | 4 | 858 | 79.52 |
| Peter J. Stuckey | 5 | 4368 | 457.58 |