Progress in Computing Applications(PCA)

DLINE Journals portal

Home

New Journals

Browse Journals

Journal Prices

For Authors

Print ISSN:
Online ISSN:

About PCA
	DLINE Portal Home Home Aims & Scope Editorial Board Current Issue Next Issue Previous Issue Sample Issue Upcoming Conferences Self-archiving policy Alert Services Be a Reviewer Publisher Paper Submission Subscription Contact us

How To Order
	Order Online Price Information Request for Complimentary Print Copy

For Authors
	Guidelines for Contributors Online Submission Call for Papers Author Rights

RELATED JOURNALS

Journal of Digital Information Management (JDIM)

Journal of Multimedia Processing and Technologies (JMPT)

International Journal of Web Application (IJWA)

Progress in Computing Applications(PCA)

Abstract Data Type Analysis Using Shape Invariants

Jan Reineke
Saarland University Im Stadtwald - GebÃƒÂ¤ude E1 3 66041 SaarbrÃƒÂ¼cken, Germany

Abstract: The purpose of Shape Analysis is to determine the shape invariant, that is, the structural properties of the heap for programs that deal with pointers and the allocation of the heap. More recently, very accurate shape analysis algorithms have been developed to prove the partial accuracy of the programs that manipulate the heap. In this section, we will look at how shape analysis can be used to analyze the abstract data type (ADT). We will use the ADT as an example because it is commonly used and found in most major data types libraries, such as STL, Java API, and LEDA. We formalise our idea of the ADT Set using the following algebras. Two prototype C set implementations are presented. One is based on lists, and the other is based on trees. We will create a parametric shape analysis framework to perform the analyses that prove the compliance of these two implementations.

Keywords: Shape Analysis, Abstract Data Type, Data Libraries Abstract Data Type Analysis Using Shape Invariants

DOI:https://doi.org/10.6025/pca/2024/13/1/7-25

Full_Text PDF 2.18 MB Download: 7 times

References:

[1] David R. Chase., Mark Wegman., and Kenneth Zadeck, F. (1990). Analysis of pointers and structures. In PLDI ’90: Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation (pp. 296-310). New York, NY, USA: ACM Press.
[2] Hartmut Ehrig and Bernd Mahr. (1985). Fundamentals of Algebraic Specification I. Secaucus, NJ, USA: Springer-Verlag New York, Inc.
[3] Hartmut Ehrig and Bernd Mahr. (1990). Fundamentals of Algebraic Specification 2: Module Specifications and Constraints. New York, NY, USA: Springer-Verlag New York, Inc.
[4] Rakesh Ghiya and Laurie J. Hendren. (1996). Is it a tree, a dag, or a cyclic graph? a shape analysis for heap-directed pointers in c. In POPL ’96: Proceedings of the 23rd ACM SIGPLANSIGACT symposium on Principles of programming languages (pp. 115). New York, NY, USA: ACM Press.
[5] Tal Lev-Ami. (2000). TVLA: A framework for Kleene based static analysis. Master’s thesis, TelAviv University, Tel-Aviv, Israel.
[6] Tal Lev-Ami, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm. (2000). Putting static analysis to work for verification: A case study. In ISSTA ’00: Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis (pp. 26-38). New York, NY, USA: ACM Press.
[7] Tal Lev-Ami and Mooly Sagiv. (2000). TVLA: A system for implementing static analyses. In SAS ’00: Proceedings of the 7th International Symposium on Static Analysis (pp. 280-301). London, UK: Springer-Verlag.
[8] Jacques Loeckx, Hans-Dieter Ehrich, and Markus Wolf. (1997). Specification of abstract data types. New York, NY, USA: John Wiley & Sons, Inc.
[9] Patrick Lam, Viktor Kuncak, and Martin Rinard. (2004). Generalized typestate checking using set interfaces and pluggable analyses.
[10] Roman Manevich. (2003). Data structures and algorithms for efficient shape analysis. Master’s thesis, Tel-Aviv University, School of Computer Science, Tel-Aviv, Israel. Retrieved from http:// www.cs.tau.ac.il/rumster/msc_thesis.pdf.
[11] Sun Microsystems. (2004). Java 2 platform standard edition 5.0 API specification. Retrieved from http://java.sun.com/j2se/1.5.0/docs/api/.
[12] Kurt Mehlhorn and Stefan Näher. (1999). LEDA - A Platform for Combinatorial and Geometric Computing. Cambridge University Press.
[13] David R. Musser and Atul Saini. (1996). STL tutorial and reference guide (Addison-Wesley professional computing series). Addison-Wesley.
[14] Jan Reineke. (2005). Shape analysis of sets. Master’s thesis, Universität des Saarlandes, Germany. Retrieved from http://rw4.cs.uni-sb.de/reineke/publications/MasterReineke.pdf.
[15] Noam Rinetzky and Mooly Sagiv. (2001). Interprocedural shape analysis for recursive programs. Lecture Notes in Computer Science, 2027, 133-149.
[16] Mooly Sagiv., Thomas Rep.s, and Reinhard Wilhelm. (1999). Parametric shape analysis via 3- valued logic. In Symposium on Principles of Programming Languages (pp. 105-118).
[17] Mooly Sagiv., Thomas Reps., and Reinhard Wilhelm. (2002). Parametric shape analysis via 3- valued logic. ACM Transactions on Programming Languages and Systems, 24(3), 217-298.

DLINE Journals portal