Abstract
We review how the dependence upon semantics has been taken into account in abstract interpretation based program analysis and next propose to design general purpose abstract interpreters taking semantics as a parameter, either that of the program to be analyzed or that of a programming language.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky and C. Hankie. An introduction to abstract interppetation, ch. 1. Ellis Horwood, 1987.
G.L. Burn, C.L. Hankin, and S. Abramsky. Strictness analysis of higher-order functions. Sci. Comput. Prog., 7:249–278, 1986.
P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, ch. 10, pp. 303–342. Prentice-Hall, 1981.
P. Cousot. Design of semantics by abstract interpretation, invited address. In Mathematical Foundations of Programming Semantics, Thirteenth Annual Conference (MFPS XIII), Carnegie Mellon University, Pittsburgh, Pennsylvania, 1997.
P. Cousot. Types as abstract interpretations, invited paper. In 24 th POPL, pp. 316–331, Paris, 1997. ACM Press.
P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4 th POPL, pp. 238–252, Los Angeles, Calif., 1977. ACM Press.
P. Cousot and R. Cousot. Automatic synthesis of optimal invariant assertions: mathematical foundations. In ACM Symposium on Artificial Intelligence & Programming Languages, Rochester, N.Y., SIGPLAN Notices 12(8):1–12, 1977.
P. Cousot and R. Cousot. Static determination of dynamic properties of recursive procedures. In E.J. Neuhold, editor, IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., Canada, pp. 237–277. North-Holland, 1977.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6 th POPL, pp. 269–282, San Antonio, Texas, 1979. ACM Press.
P. Cousot and R. Cousot. Semantic analysis of communicating sequential processes. In J.W. de Bakker and J. van Leeuwen, editors, 7 th ICALP, LNCS 85, pp. 119–133. Springer-Verlag, 1980.
P. Cousot and R. Cousot. Invariance proof methods and analysis techniques for parallel programs. In A.W. Biermann, G. Guiho, and Y. Kodratoff, editors, Automatic Program Construction Techniques, ch. 12, pp. 243–271. Macmillan, 1984.
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Prog., 13(2-3):103–179, 1992. (The editor of JLP has mistakenly published the unreadable galley proof. For a correct version of this paper, see http: //vvw.dmi. ens.fr/-cousot.).
P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Logic and Comp., 2(4):511–547, 1992.
P. Cousot and R. Cousot.Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In M. Bruynooghe and M. Wirsing, editors, Proc. Int. Work. PLILP'92, Leuven, Belgium, LNCS 631, pages 269–295. Springer-Verlag, 1992.
P. Cousot and R. Cousot. Galois connection based abstract interpretations for strictness analysis, invited paper. In D. Bjørner, M. Broy, and I.V. Pottosin, editors, Proc. FMPA, Academgorodok, Novosibirsk, Russia, LNCS 735, pages 98127. Springer-Verlag, 1993.
P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In Proc. 1994 ICCL, Toulouse, France, pp. 95–112. IEEE Comp. Soc. Press, 1994.
P. Cousot and R. Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form, invited paper. In P. Wolper, editor, Proc. 7 th Int. Conf. CAV '95, Liège, Belgium, LNCS 939, pp. 293–308. Springer-Verlag, 1995.
P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Proc. 7 th FPCA, pp. 170–181, La Jolla, Calif, 1995. ACM Press.
S.K. Debray. Formal bases for dataflow analysis of logic programs. In G. Levi, editor, Advances in Logic Programming Theory, International Schools for Computer Scientists, section 3, pp. 115–182. Clarendon Press, 1994.
A. Deutsch. A storeless model of aliasing and its abstraction using finite representations of right-regular equivalence relations. In Proc. 1992 ICCL, Oakland, Calif., pp. 2–13. IEEE Comp. Soc. Press, 1992.
N. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall, 1993.
N.D. Jones and F. Nielson. Abstract interpretation: a semantics-based tool for program analysis. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors, Semantic Modelling, volume 4 of Handbook of Logic in Computer Science, ch. 5, pp. 527–636. Clarendon Press, 1995.
A. Mycroft. Abstract Interpretation and Optimising Transformations for Applicative Programs. Ph.D. Dissertation, CST-15-81, Department of Computer Science, University of Edinburgh, Edinburg, Scotland, 1981.
F. Nielson. Two-level semantics and abstract interpretation. TCS-Fund. St., 69:117–242, 1989.
A. Venet. Abstract cofibred domains: Application to the alias analysis of untyped programs. In R. Cousot and D.A. Schmidt, editors, Proc. SAS'96, Aachen, Germany, LNCS 1145, pp. 368–382. Springer-Verlag, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cousot, P. (1997). Abstract interpretation based static analysis parameterized by semantics. In: Van Hentenryck, P. (eds) Static Analysis. SAS 1997. Lecture Notes in Computer Science, vol 1302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032759
Download citation
DOI: https://doi.org/10.1007/BFb0032759
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63468-3
Online ISBN: 978-3-540-69576-9
eBook Packages: Springer Book Archive