Abstract
Fixpoint computation is a major issue in abstract interpretation. However, little attention has been devoted to the design and implementation of efficient general purpose fixpoint algorithms. This paper provides an experimental evaluation of several general-purpose optimization techniques: stabilization detection, manipulation of the sets of call patterns, and caching of abstract operations. All techniques can be included in a general fixpoint algorithm which can then be proven correct once for all and instantiated to a large variety of abstract semantics. For the sake of the experiments, we focus on a single abstract semantics for Prolog and shows the instantiations of the general-purpose algorithms to this semantics. The experiments are done on two abstract domains and a significant set of benchmarks programs. They seem to demonstrate the practical value of the approach.
Part of this research was done when O. Degimbe and L. Michel were visiting Brown university.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
M. Bruynooghe. A practical framework for the abstract interpretation of logic programs. Journal of Logic Programming, 10(2):91–124, February 1991.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc.POPL'77, January 1977.
V. Englebert, B. Le Charlier, D. Roland, and P. Van Hentenryck. Generic abstract interpretation algorithms for Prolog: Two optimization techniques and their experimental evaluation. December 1991. To appear in Software Practice and Experience.
M. Hermenegildo, R. Warren, and S. Debray. Global Flow Analysis as a Practical Compilation Tool. Journal of Logic Programming, 13(4):349–367, 1992.
N.D. Jones and A. Mycroft. Dataflow analysis of applicative programs using minimal function graphs. In Proc. POPL'86, 1986.
B. Le Charlier, K. Musumbu, and P. Van Hentenryck. Efficient and accurate algorithms for the abstract interpretation of Prolog programs. Technical Report 37/90, Namur, Belgium, 1990.
B. Le Charlier, K. Musumbu, and P. Van Hentenryck. A generic abstract interpretation algorithm and its complexity analysis. In Proc. ICLP'91, Paris, France, June 1991. MIT Press.
B. Le Charlier and P. Van Hentenryck. Experimental Evaluation of a Generic Abstract Interpretation Algorithm for Prolog. To appear in TOPLAS.
B. Le Charlier and P. Van Hentenryck. A universal top-down fixpoint algorithm. Technical Report 92-22, Institute of Computer Science, University of Namur, Belgium, April 1992.
K. Marriott and H. SØndergaard. Semantics-based dataflow analysis of logic programs. In G. Ritter, editor, Information Processing'89, pages 601–606, San Fransisco, California, 1989.
K. Musumbu. Interprétation Abstraite de Programmes Prolog. PhD thesis, Institute of Computer Science, University of Namur, Belgium, September 1990. In French.
W. Winsborough. Multiple specialization using minimal-function graph semantics. Journal of Logic Programming, 13(4), February 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Le Charlier, B., Degimbe, O., Michel, L., Van Hentenryck, P. (1993). Optimization techniques for general purpose fixpoint algorithms practical efficiency for the abstract interpretation of Prolog. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_26
Download citation
DOI: https://doi.org/10.1007/3-540-57264-3_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57264-0
Online ISBN: 978-3-540-48027-3
eBook Packages: Springer Book Archive