Agostino Cortesi
Gilberto Filé
Francesco Ranzato
Roberto Giacobazzi
Abstract
Reduced product of abstract domains is a rather well-known operation for domain composition in abstract interpretation. In this article, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. Complementation provides as systematic way to design new abstract domains, and it allows to systematically decompose domains. Also, such an operation allows to simplify domain verification problems, and it yields space-saving representations for complex domains. We show that the complement exists in most coses, and we apply complementation to three well-know abstract domains, notably to Cousot and Cousot's interval domain for integer variable analysis, to Cousot and Cousot's domain for comportment analysis of functional languages, and to the domain Sharing for aliasing analysis of logic languages.
- ARMSTRONG, T., MARRIOTT, I~., SCHACHTE, P., AND SONDERGAARD, H. 1994. Boolean functions for dependency analysis: Algebraic properties and efficient representation. In Proceedings of the 1st International Static Analysis Symposium (SAS 'gJ), B. Le Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 266-280.Google Scholar
- BIRKHOFF, G. 1967. Lattice Theory. AMS Colloquium Publication, 3rd edition. AMS, Providence, R.I.Google Scholar
- CODISH, M., MULKERS, A., BRUYNOOGHE, M., GARCfA DE LA BANDA, M., AND HERMENEGILDO, M. 1995. Improving abstract interpretations by combining domains. A CM Trans. Program. Lang. Syst. 17, 1, 28-44. Google Scholar
- COMINI, M. AND LEVI, G. 1994. An algebraic theory of observables. In Proceedings of the 199~ International Logic Programming Symposium (ILPS '9~ ), M. Bruynooghe, Ed. The MIT Press, Cambridge, Mass., 172-186. Google Scholar
- CORTESI, A., FILI~, G., AND WINSBOROUGH, W. 1992. Comparison of abstract interpretations. In Proceedings of the 19th International Colloquium on Automata, Languages and Programming (ICALP '92), W. Kuich, Ed. Lecture Notes in Computer Science, vol. 623. Springer-Verlag, Berlin, 521-532. Google Scholar
- CORTESI, A., FILI~, G., AND WINSBOROUGH, W. 1996. Optimal groundness analysis using propositionM logic. J. Logic Program. 27, 2, 137-167.Google Scholar
- COUSOT, P. 1978. M6thodes It6ratives de Construction et d'Approximation de Points Fixes d'Op6rateurs Monotones sur un Treillis, Analyse S6mantique des Programmes. Ph.D. thesis, Universit6 Scientifique et M6dicale de Grenoble, Grenoble, France.Google Scholar
- COUSOT, P. AND COUSOT, R. 1976. Static determination of dynamic properties of programs. In Proceedings of the 2nd International Symposium on Programming. Dunod, Paris, 106-130.Google Scholar
- COUSOT, P. AND COUSOT, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Jth ACM Symposium on Principles of Programming Languages (POPL '77). ACM Press, New York, 238-252. Google Scholar
- COUSOT, P. AND COUSOT, R. 1979. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL '79). ACM Press, New York, 269-282. Google Scholar
- COUSOT, P. AND COUSOT, R. 1992a. Abstract interpretation and application to logic programs. J. Logic Program. 13, 2-3, 103-179. Google Scholar
- COUSOT, P. AND COUSOT, R. 1992b. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th A CM Symposium on Principles of Programming Languages (POPL '92). ACM Press, New York, 83-94. Google Scholar
- COUSOT, P. AND COUSOT, R. 1994. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). In Proceedings of the IEEE International Conference on Computer Languages (ICCL 'gJ). IEEE Computer Society Press, Los Alamitos, Calif., 95-112.Google Scholar
- DART, P. 1988. Dependency analysis and query interfaces for deductive databases. Ph.D. thesis, Univ. of Melbourne, Melbourne, Australia.Google Scholar
- DART, P. 1991. On derived dependencies and connected databases. J. Logic Program. 11, 2, 163-188. Google Scholar
- DAVEY, B. A. AND PRIESTLEY, H. A. 1990. Introduction to Lattices and Order. Cambridge University Press, Cambridge, U.K.Google Scholar
- DWINGER, P. 1954. On the closure operators of a complete lattice. Indagationes Mathematicae 16, 560-563.Google Scholar
- FILI~, G., GIACOBAZZI, R., AND RANZATO, F. 1996. A unifying view of abstract domain design. A CM Comput. Surv. 28, 2, 333-336. Google Scholar
- FILI~, G. AND RANZATO, F. 1996. Complementation of abstract domains made easy. In Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP '96), M. Maher, Ed. The MIT Press, Cambridge, Mass., 348-362.Google Scholar
- FRINK, O. 1962. Pseudo-complements in semi-lattices. Duke Math. J. 29, 505-514.Google Scholar
- GIACOBAZZI~ R. 1996. "Optimal" collecting semantics for analysis in a hierarchy of logic program semantics. In Proceedings of the 13th International Symposium on Theoretical Aspects of Computer Science (STACS '96), C. Puech and R. Reischuk, Eds. Lecture Notes in Computer Science, vol. 1046. Springer-Verlag, Berlin, 503-514. Google Scholar
- GIACOBAZZI~ R., PALAMIDESSI~ C., AND RANZATO~ F. 1996. Weak relative pseudo-complements of closure operators. Algebra Universalis 36, 3, 405-412.Google Scholar
- GIACOBAZZI~ R. AND RANZATO~ F. 1996. Complementing logic program semantics. In Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP '96), M. Hanus and M. Rodrfguez Artalejo, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, 238-253. Google Scholar
- GIERZ~ G., HOFMANN~ K. H., KEIMEL~ K., LAWSON~ J. D., MISLOVE~ M., AND SCOTT~ D. S. 1980. A Compendium of Continuous Lattices. Springer-Verlag, Berlin.Google Scholar
- GRXTZER, G. 1978. General Lattice Theory. Birkhguser Verlag, Basel, Switzerland.Google Scholar
- HUNT, S. 1990. PERs generalize projections for strictness analysis. In Proceedings of the 1990 Glasgow Functional Programming Workshop, S. Peyton Jones, G. Hutton, and C. K. Holst, Eds. Workshops in Computing. Springer-Verlag, Berlin, 156-168.Google Scholar
- JACOBS, D. AND LANGEN, A. 1989. Accurate and efficient approximation of variable aliasing in logic programs. In Proceedings of the 1989 North American Conference on Logic Programming (NACLP '89), E. L. Lusk and R. A. Overbeek, Eds. The MIT Press, Cambridge, Mass., 154-165.Google Scholar
- JACOBS, D. AND LANGEN, A. 1992. Static analysis of logic programs for independent AND- parallelism. J. Logic Program. 13, 2-3, 154-165. Google Scholar
- KAM, J. B. AND ULLMAN, J. D. 1977. Monotone data flow analysis frameworks. Acta Informatica 7, 305-317.Google Scholar
- KILDALL, G. A. 1973. A unified approach to global program optimization. In Conference Record of the 1st ACM Symposium on Principles of Programming Languages (POPL '73). ACM Press, New York, 194-206. Google Scholar
- MARCHIORI, E. 1996. Prime factorizations of abstract domains using first order logic. In Proceedings of the 5th International Conference on Algebraic and Logic Programming (ALP '96), M. Hanus and M. Rodrfguez Artalejo, Eds. Lecture Notes in Computer Science. Springer-Verlag, Berlin, 209-223. Google Scholar
- MARRIOTT, K. AND SONDERGAARD, H. 1993. Precise and efficient groundness analysis for logic programs. ACM Lett. Program. Lang. Syst. 2, 1-4, 181-196. Google Scholar
- MORGADO, J. 1962. Note on complemented closure operators of complete lattices. Portugalice- Mathematica 21, 3, 135-142.Google Scholar
- MUTHUKUMAR, K. AND HERMENEGILDO, M. 1991. Combined determination of sharing and freeness of program variables through abstract interpretation. In Proceedings of the 8th International Conference on Logic Programming (ICLP '91 ), K. Furukawa, Ed. The MIT Press, Cambridge, Mass., 49-63.Google Scholar
- MYCROFT, A. 1980. The theory and practice of transforming call-by-need into call-by-value. In Proceedings of the ~th International Symposium on Programming, B. Robinet, Ed. Lecture Notes in Computer Science, vol. 83. Springer-Verlag, Berlin, 270-281. Google Scholar
- MYCROFT, A. 1981. Abstract interpretation and optimising transformations for applicative programs. Ph.D. thesis, CST-15/81, Univ. of Edinburgh, Edinburgh, Scotland.Google Scholar
- MYCROFT, A. 1993. Completeness and predicate-based abstract interpretation. In Proceedings of the A CM Symposium on Partial Evaluation and Program Manipulation (PEPM '93). ACM Press, New York, 179-185. Google Scholar
- NIELSON, F. 1985. Tensor products generalize the relational data flow analysis method. In Proceedings of the ~th Hungarian Computer Science Conference, M. Aratd, I. K~tai, and L. Varga, Eds. 211-225.Google Scholar
- SUNDARARAJAN, R. AND CONERY, J. 1992. An abstract interpretation scheme for groundness, freeness, and sharing analysis of logic programs. In Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science (FST~iTCS '92), R. Shyamasundar, Ed. Lecture Notes in Computer Science, vol. 652. Springer-Verlag, Berlin, 203-216. Google Scholar
- VARLET, J. 1963. Contribution ~ l'6tude des treillis pseudo-compl6ment6s et des treillis de Stone. Mdmoires de la Socidtd Royale des Sciences de Liege 8, 4, 1-71.Google Scholar
- WADLER, P. AND HUGHES, R. J. iV{. 1987. Projections for strictness analysis. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA '87), G. Kahn, Ed. Lecture Notes in Computer Science, vol. 274. Springer-Verlag, Berlin, 385-407. Google Scholar
- WARD, ~/{. 1942. The closure operators of a lattice. Ann. Math. 43, 2, 191-196.Google Scholar
- YI, K. AND HARRISON, W. L. 1993. Automatic generation and management of interprocedural program analyses. In Conference Record of the 20th A CM Symposium on Principles of Programming Languages (POPL '93). ACM Press, New York, 246-259. Google Scholar
Index Terms
- Complementation in abstract interpretation
Recommendations
A²I: abstract² interpretation
The fundamental idea of Abstract2 Interpretation (A2I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A2I is generally meant to use abstract interpretation to ...
Descriptional complexity of determinization and complementation for finite automata
CATS 2011: Proceedings of the Seventeenth Computing on The Australasian Theory Symposium - Volume 119In this paper we study the subset construction that transforms nondeterministic finite automata (NFA) to deterministic finite automata (DFA). It is well known that given a n-state NFA, the subset construction algorithm produces a 2n-state DFA in the ...
Descriptional complexity of determinization and complementation for finite automata
CATS '11: Proceedings of the Seventeenth Computing: The Australasian Theory Symposium - Volume 119In this paper we study the subset construction that transforms nondeterministic finite automata (NFA) to deterministic finite automata (DFA). It is well known that given a n-state NFA, the subset construction algorithm produces a 2n-state DFA in the ...
Reviews
D. John Cooke
Abstract interpretation is concerned with the semantics of programming languages at different levels of abstraction. The idea is to construct abstract domains that, in some sense, approximate the concrete domain in which the full programming language semantics are defined and use them to simplify the analyses of programs. Of course, properties that are the subject of any given program analysis must behave in the abstract domain in ways consistent with the underlying concrete semantics. Starting from a formalization of abstraction, defined in terms of Galois insertions, and the reduced product of domains, the authors expound the use of pseudocomplementation to decompose domains into a minimal conjunction of more basic domains. (They observe that the domains under investigation may not have been constructed by the reverse of this process.) This is not possible in the standard theory of abstract interpretation, but the authors claim that their construction can be applied in most cases of interest. This supports the inductive calculation of complements (saturation points of increasing sequences of closure operators) in finite sets, and an algorithm is given for finding minimal decompositions of finite concrete domains. The theory is then applied to integer variable analysis in imperative programs, to comportment (“feature”) analysis in functional programs (in which the strictness and termination domains are complementary), and to the analysis of sharing and groundedness in logic programs. Although the paper contains a handful of grammatical errors, it is well written and easy to understand, provided you know your domain theory.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments