Abstract
We develop abstract interpretation from topological principles by relaxing the definitions of open set and continuity; key results still hold. We study families of closed and open sets and show they generate post- and pre-condition analyses, respectively. Giacobazzi’s forwards- and backwards-complete functions are characterized by the topologically closed and continuous maps, respectively. Finally, we show that Smyth’s upper and lower topologies for powersets induce the overapproximating and underapproximating transition functions used for abstract-model checking.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abramsky, S.: Domain theory in logical form. Ann. Pure Appl. Logic 51, 1–77 (1991)
Benton, N.: Strictness logic and polymorphic invariance. In: Proc. Logical Found. Comp. Sci, pp. 33–44 (1992)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Cleaveland, R., Iyer, P., Yankelevich, D.: Optimality in abstractions of model checking. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983. Springer, Heidelberg (1995)
Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis, pp. 303–342. Prentice-Hall, Englewood Cliffs (1981)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs. In: Proc. 4th ACM Symp. POPL, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E.J. (ed.) Formal Description of Programming Concepts, pp. 238–277. North-Holland, Amsterdam (1978)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6th ACM Symp. POPL, pp. 269–282 (1979)
Cousot, P., Cousot, R.: Higher-order abstract interpretation. In: Proceedings IEEE Int. Conf. Computer Lang. (1994)
Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Systems 19, 253–291 (1997)
Dybjer, P.: Inverse image analysis generalises strictness analysis. Information and Computation 90, 194–216 (1991)
Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47, 361–416 (2000)
Gunter, C., Scott, D.S.: Semantic domains. In: Handbook of Theoretical Computer Science, vol. B, pp. 633–674. MIT Press, Cambridge (1991)
Hunt, S.: Frontiers and open sets in abstract intepretation. In: Proc. ACM Symp. Functional Prog. and Comp. Architecture, pp. 194–216 (1989)
Jensen, T.: Abstract Interpretation in Logical Form. PhD thesis, Imperial College, London (1992)
Johnstone, P.: Stone Spaces. Cambridge University Press, Cambridge (1986)
Reynolds, J.C.: Notes on a lattice-theoretic approach to the theory of computation. Technical report, Computer Science, Syracuse University (1972)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS 24, 217–298 (2002)
Schmidt, D.A.: Comparing completeness properties of static analyses and their logics. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 183–199. Springer, Heidelberg (2006)
Schmidt, D.A.: Underapproximating predicate transformers. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 127–143. Springer, Heidelberg (2006)
Schmidt, D.A.: A calculus of logical relations for over- and underapproximating static analyses. Science of Computer Programming 64, 29–53 (2007)
Smyth, M.B.: Effectively given domains. Theoretical Comp. Sci. 5, 257–274 (1977)
Smyth, M.B.: Powerdomains and predicate transformers: a topological view. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 662–675. Springer, Heidelberg (1983)
Willard, S.: General Topology. Dover Publications (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, D.A. (2009). Abstract Interpretation from a Topological Perspective. In: Palsberg, J., Su, Z. (eds) Static Analysis. SAS 2009. Lecture Notes in Computer Science, vol 5673. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03237-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-03237-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03236-3
Online ISBN: 978-3-642-03237-0
eBook Packages: Computer ScienceComputer Science (R0)