Logical Characterizations of Heap Abstractions

Title: Logical Characterizations of Heap Abstractions

Research Question: Can 3-valued logical structures, used in heap abstractions, be characterized using first-order logic with transitive closure?

Methodology: The researchers used logical characterizations to examine the expressiveness of 3-valued structures in heap abstractions. They proposed a no-standard ("supervaluational") semantics for 3-valued first-order logic, which was more precise than a conventional 3-valued semantics.

Results: The researchers were able to characterize 3-valued structures using formulas in first-order logic with transitive closure. They also demonstrated that the supervaluational semantics could be effectively implemented using existing theorem provers.

Implications: This research has implications for the field of abstract interpretation, particularly in the areas of shape analysis and concurrency. The results provide a better understanding of the expressiveness of 3-valued structures and offer a more precise semantics for interpreting abstract values. This can lead to improved verification tools, program optimizers, and program-understanding tools.

Link to Article: https://arxiv.org/abs/0312014v3 Authors: arXiv ID: 0312014v3