Logical Characterizations of Heap Abstractions

Title: Logical Characterizations of Heap Abstractions

Research Question: How can we characterize the expressive power of 3-valued logical structures used in heap abstractions?

Methodology: The researchers used 3-valued first-order logic to characterize the expressive power of the logical structures. They also introduced a non-standard (super-valuation) semantics for 3-valued first-order logic, which was more precise and could be effectively implemented using existing theorem provers.

Results: The researchers showed that it is always possible to give a logical characterization written in first-order logic with transitive closure for a well-defined class of 3-valued structures. This class includes all the 3-valued structures that have been used in heap abstractions.

Implications: This work provides a logical framework for understanding the expressive power of 3-valued logical structures used in heap abstractions. It also has broader applications to any abstraction where concrete states of a system are represented by finite 2-valued logical structures, and abstraction is performed using the mechanisms described in the paper.

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