Sweeping in Abstract Interpretation
Pages 25 - 36
Abstract
In this paper we present how sweeping line techniques, which are very popular in computational geometry, can be adapted for static analysis of computer software by abstract interpretation. We expose how concept of the sweeping line can be used to represent elements of a numerical abstract domain of boxes, which is a disjunctive refinement of a well known domain of intervals that allows finite number of disjunctions. We provide a detailed description of the representation along with standard domain operations algorithms. Furthermore we introduce very precise widening operator for the domain. Additionally we show that the presented idea of the representation based on sweeping line technique is a generalisation of the representation that uses Linear Decision Diagrams (LDD), which is one of possible optimisations of our idea. We also show that the presented widening operator is often more precise than the previous one.
References
[1]
Bagnara, R., Hill, P. and Zaffanella, E., Widening operators for powerset domains. International Journal on Software Tools for Technology Transfer (STTT). v9. 413-414.
[2]
Bentley, J.L. and Ottmann, T.A., Algorithms for reporting and counting geometric intersections. IEEE Trans. Comput. v28. 643-647.
[3]
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D. and Rival, X., The Essence of Computation: Complexity, Analysis, Transformation. In: Lecture Notes in Computer Science, vol. 2566. Springer-Verlag. pp. 85-108.
[4]
P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106-130. Dunod, Paris, France, 1976.
[5]
Cousot, P. and Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: The Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, NY. pp. 238-252.
[6]
Cousot, P. and Cousot, R., Comparing the galois connection and widening/narrowing approaches to abstract interpretation. In: Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, Springer-Verlag. pp. 269-295.
[7]
Cousot, P. and Halbwachs, N., Automatic discovery of linear restraints among variables of a program. In: The Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, NY. pp. 84-97.
[8]
Fortune, S., A sweepline algorithm for voronoi diagrams. In: Proceedings of the second annual symposium on Computational geometry, ACM. pp. 313-322.
[9]
Fulara, J., Durnoga, K., Jakubczyk, K. and Schubert, A., Relational abstract domain of weighted hexagons. Electron. Notes Theor. Comput. Sci. v267. 59-72.
[10]
Gurfinkel, A. and Chaki, S., Boxes: a symbolic abstract domain of boxes. In: Proceedings of the 17th international conference on Static analysis, Springer-Verlag. pp. 287-303.
[11]
Howe, J.M., King, A. and Lawrence-Jones, C., Quadtrees as an abstract domain. Electron. Notes Theor. Comput. Sci. v267. 89-100.
[12]
Logozzo, F. and Fähndrich, M., Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: Proceedings of the 2008 ACM symposium on Applied computing, ACM. pp. 184-188.
[13]
Mauborgne, L. and Rival, X., . In: Trace partitioning in abstract interpretation based static analyzers, Springer. pp. 5-20.
[14]
Miné, A., The octagon abstract domain. Higher Order Symbol. Comput. v19. 31-100.
[15]
Sankaranarayanan, S., Ivancic, F., Shlyakhter, I. and Gupta, A., Static analysis in disjunctive numerical domains. In: LNCS, vol. 4134. Springer. pp. 3-17.
[16]
Simon, A., King, A. and Howe, J.M., Two variables per linear inequality as an abstract domain. In: LOPSTR¿02: Proceedings of the 12th international conference on Logic based program synthesis and transformation, Springer-Verlag. pp. 71-89.
Index Terms
- Sweeping in Abstract Interpretation
Index terms have been assigned to the content through auto-classification.
Recommendations
Bound Analysis for Whiley Programs
The Whiley compiler can generate naive C code, but the code is inefficient because it uses infinite integers and dynamic array sizes. Our project goal is to build up a compiler that can translate Whiley programs into efficient OpenCL code with fixed-...
The octagon abstract domain
This article presents the octagon abstract domain , a relational numerical abstract domain for static analysis by abstract interpretation. It allows representing conjunctions of constraints of the form X Y c where X and Y range among program ...
SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities
We introduce SubPolyhedra (SubPoly), a new family of numerical abstract domains to infer and propagate linear inequalities. The key insight is that the reduced product of linear equalities and intervals produces powerful yet scalable analyses. Abstract ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier B.V. © 2012.
Publisher
Elsevier Science Publishers B. V.
Netherlands
Publication History
Published: 01 December 2012
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 28 Sep 2024
Other Metrics
Citations
View Options
View options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in