Home |
Personal Info |
Papers |
Teaching |
Links |
Decomposing Non-Redundant Sharing by Complementation
Enea Zaffanella
Servizio IX Automazione
Università di Modena
Italy
Patricia M. Hill
School of Computer Studies
University of Leeds
Leeds, LS2 9JT
United Kingdom
Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Abstract:
Complementation, the inverse of the reduced product operation, is a relatively new technique for systematically finding minimal decompositions of abstract domains. Filé 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 operation was still SH, they concluded that PS was too abstract for this. Here, we show that the source of this difficulty 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, the difficulties vanish if our non-redundant version of SH, SHρ, is substituted for SH. To establish the results for SHρ, we define a general schema for subdomains of SH that includes SHρ and Def as special cases. This sheds new light on the structure of SHρ and exposes a natural though unexpected connection between Def and SHρ. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.Keywords: Abstract Interpretation, Domain Decomposition, Complementation, Sharing Analysis.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on January 22, 2000, 20:38:36.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links