Logical Characterizations of Heap Abstractions

Title: Logical Characterizations of Heap Abstractions

Research Question: How can we characterize and express the 3-valued structures that arise in heap abstractions using logical formulas?

Methodology: The researchers used 3-valued first-order logic with transitive closure to characterize the 3-valued structures that arise in heap abstractions. They also introduced a non-standard (super-valuation) semantics for 3-valued first-order logic, which is more precise than a conventional 3-valued semantics.

Results: The researchers showed that 3-valued structures can be characterized using formulas in first-order logic with transitive closure. They also demonstrated that their non-standard semantics can be effectively implemented using existing theorem provers.

Implications: These results provide insights into the expressiveness of 3-valued structures in heap abstractions and have 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 Sections 2 and 3.1 of the paper.

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