Name
Abstract | ||
|---|---|---|
A static shape analysis is presented that can prove the absence of NULL- and dangling pointer dereferences in standard algorithms on lists, trees and graphs. It is conceptually simpler than other analyses that use symbolically represented logic to describe the heap. Instead, it represents the heap as a single graph and a Boolean formula. The key idea is to summarize two nodes by calculating their common points-to information, which is done using the recently proposed fold and expand operations. The force of this approach is that both, fold and expand, retain relational information between points-to edges, thereby essentially inferring new shape invariants. We show that highly precise shape invariants can be inferred using off-the-shelf SAT-solvers. Cheaper approximations may augment standard points-to analysis used in compiler optimisations. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-37051-9_5 | CC |
Keywords | Field | DocType |
points-to edge,precise shape invariants,standard points-to analysis,cheaper approximation,standard algorithm,static shape analysis,relational information,expand-based shape analysis,boolean formula,new shape invariants,common points-to information | Boolean function,Discrete mathematics,Separation logic,Standard algorithms,Computer science,Algorithm,Theoretical computer science,Heap (data structure),Compiler,Dangling pointer,True quantified Boolean formula,Shape analysis (digital geometry) | Conference |
Volume | ISSN | Citations |
7791 | 0302-9743 | 3 |
PageRank | References | Authors |
0.42 | 16 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Holger Siegel | 1 | 11 | 1.92 |
| Axel Simon | 2 | 168 | 13.32 |