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 dificulties 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
Part of this work was supported by EPSRC grant GR/M05645.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. In P. Van Hentenryck, editor, Static Analysis: Proceedings of the 4th International Symposium, volume 1302 of Lecture Notes in Computer Science, pages 53–67, Paris, France, 1997. Springer-Verlag, Berlin.
R. Bagnara and P. Schachte. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In A. M. Haeberer, editor, Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (AMAST’98)”, volume 1548 of Lecture Notes in Computer Science, pages 471–485, Amazonia, Brazil, 1999. Springer-Verlag, Berlin.
M. Codish and H Sündergaard. The Boolean logic of set sharing analysis. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Principles of Declarative Programming, volume 1490 of Lecture Notes in Computer Science, pages 89–100, Pisa, Italy, 1998. Springer-Verlag, Berlin.
A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. In A. Mycroft, editor, Static Analysis: Proceedings of the 2nd International Symposium, volume 983 of Lecture Notes in Computer Science, pages 100–117, Glasgow, UK, 1995. Springer-Verlag, Berlin.
A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM Transactions on Programming Languages and Systems, 19(1):7–47, 1997.
A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation for comparing static analyses. Theoretical Computer Science, 202(1&2):163–192, 1998.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269–282, 1979.
G. Filé and F. Ranzato. Complementation of abstract domains made easy. In M. Maher, editor, Logic Programming: Proceedings of the Joint International Conference and Symposium on Logic Programming, MIT Press Series in Logic Programming, pages 348–362, Bonn, Germany, 1996. The MIT Press.
R. Giacobazzi and F. Ranzato. Completeness in abstract interpretation: a domain perspective. In M. Johnson, editor, Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97), volume 1349 of Lecture Notes in Computer Science, pages 231–245, Sydney, Australia, 1997. Springer-Verlag, Berlin.
R. Giacobazzi, F. Ranzato, and F. Scozzari. Complete abstract interpretations made constructive. In J. Gruska and J. Zlatuska, editors, Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS’98), volume 1450 of Lecture Notes in Computer Science, pages 366–377. Springer-Verlag, Berlin, 1998.
G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, 1980.
P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. In G. Levi, editor, Static Analysis: Proceedings of the 5th International Symposium, volume 1503 of Lecture Notes in Computer Science, pages 99–114, Pisa, Italy, 1998. Springer-Verlag, Berlin.
D. Jacobs and A. Langen. Static analysis of logic programs for independent AND parallelism. Journal of Logic Programming, 13(2&3):291–314, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zaffanella, E., Hill, P.M., Bagnara, R. (1999). Decomposing Non-redundant Sharing by Complementation. In: Cortesi, A., Filé, G. (eds) Static Analysis. SAS 1999. Lecture Notes in Computer Science, vol 1694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48294-6_5
Download citation
DOI: https://doi.org/10.1007/3-540-48294-6_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66459-8
Online ISBN: 978-3-540-48294-9
eBook Packages: Springer Book Archive