| Autor: |
Emerson, E. Allen, Namjoshi, Kedar S., Arnold, Gilad, Manevich, Roman, Sagiv, Mooly, Shaham, Ran |
| Zdroj: |
Verification, Model Checking & Abstract Interpretation (9783540311393); 2005, p33-48, 16p |
| Abstrakt: |
We consider the problem of computing the intersection (meet) of heap abstractions. This problem is useful, among other applications, to relate abstract memory states computed by forward analysis with abstract memory states computed by backward analysis. Since dynamically allocated heap objects have no static names, relating objects computed by different analyses cannot be done directly. We show that the problem of computing meet is computationally hard. We describe a constructive formulation of meet based on certain relations between abstract heap objects. The problem of enumerating those relations is reduced to finding constrained matchings in graphs. We implemented the algorithm in the TVLA system and used it to prove temporal heap properties of several small Java programs, and obtained empirical evidence showing the effectiveness of the meet algorithm. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
