Decomposing Non-Redundant Sharing

Title: Decomposing Non-Redundant Sharing

Research Question: How can we decompose the sharing domain more effectively to better understand and verify program behavior?

Methodology: The authors proposed a new method for decomposing the sharing domain (SH) into three subdomains: ground-dependency, variable independence, and set-sharing information. They used complementation, an inverse of the reduced product operation, to systematically find minimal decompositions of abstract domains.

Results: The authors found that the previous decomposition of SH into three subdomains (Fil'e and Ranzato 1996) was not optimal. They discovered that the redundancy in SH was the cause of this issue. By introducing a non-redundant version of SH, called PSD, they were able to obtain a proper decomposition. They also established a connection between PSD and a special case of their general schema for subdomains of SH.

Implications: The authors' work sheds new light on the structure of PSD and exposes a natural though unexpected connection between PSD and Def. They suggest that complementation alone is not sufficient to obtain truly minimal decompositions of domains. Instead, the right solution lies in removing redundancies by computing the quotient of the domain with respect to observable behavior and then decomposing it by complementation.

Significance: The research provides a more effective method for decomposing the sharing domain, which is crucial for understanding and verifying program behavior. The new approach offers space saving representations for domains and simplifies verification problems. It also highlights the importance of considering the underlying structure of domains and removing redundant information to obtain accurate and minimal decompositions.

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