Decomposing Non-redundant Sharing by Complementation

Complementation, the inverse of the reduced product operation, is a technique for systemfinding minimal decompositions of abstract domains. Fil´e and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen’s set-sharing domain SH . However, since the result of this n was still SH , they concluded that PS was too abstract for this. Here, we show that the source of this result lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, a proper decomposition is obtained if the non-redundant version of SH , PSD, is substituted for SH . To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of PSD and exposes a nat...

• Type: Conference
• Year: 1999
• Where: SAS
• Authors: Enea Zaffanella, Patricia M. Hill, Roberto Bagnara
• Keywords: Formal Methods, Minimal Decompositions, Pair-sharing Domain Ps, SAS 1999, Set-sharing Domain Sh