Abstract
In the abstract interpretation theory, program properties are encoded by abstract domains, and the combination of abstract domains leads to new properties to be analyzed. We propose a new method to combine numerical abstract domains based on the Minkowski sum. We provide a general framework equipped with all the necessary abstract operators for static analysis of imperative languages.
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.
References
Amato, G., Di Nardo Di Maio, S., Scozzari, F.: Numerical static analysis with soot. In: Proceedings of the ACM SIGPLAN International Workshop on State of the Art in Java Program Analysis, SOAP (2013)
Amato, G., Scozzari, F.: Jandom. https://github.com/jandom-devel/Jandom
Amato, G., Scozzari, F.: The abstract domain of parallelotopes. In: Proceedings of the NSAD 2012. ENTCS, vol. 287, pp. 17–28 (2012)
Amato, G., Scozzari, F.: Localizing widening and narrowing. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 25–42. Springer, Heidelberg (2013)
Cortesi, A., Le Charlier, B., Van Hentenryck, P.: Combinations of abstract domains for logic programming: Open product and generic pattern construction. Science of Computer Programmming 38(1–3), 27–71 (2000)
Cortesi, A., Filé, G., Winsborough, W.W.: The quotient of an abstract interpretation. Theoretical Computer Science 202(1–2), 163–192 (1998)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. 2nd Int’l Symposium on Programming, pp. 106–130 (1976)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL 1977, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the POPL 1979, pp. 269–282 (1979)
Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–549 (1992)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the POPL 1978, pp. 84–97 (1978)
Ghorbal, K., Ivančić, F., Balakrishnan, G., Maeda, N., Gupta, A.: Donut domains: efficient non-convex domains for abstract interpretation. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 235–250. Springer, Heidelberg (2012)
Goubault, E., Putot, S., Védrine, F.: Modular static analysis with zonotopes. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 24–40. Springer, Heidelberg (2012)
Maisonneuve, V., Hermant, O., Irigoin, F.: Alice: a framework to improve affine loop invariant computation. In: 5th Workshop on Invariant Generation (2014)
Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31–100 (2006)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Amato, G., Di Nardo Di Maio, S., Scozzari, F. (2015). Sum of Abstract Domains. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-17524-9_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17523-2
Online ISBN: 978-3-319-17524-9
eBook Packages: Computer ScienceComputer Science (R0)