Pentagons

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Pentagons: a weakly relational abstract domain for the efficient validation of array accesses

Full text

Pdf (171 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 2008 ACM symposium on Applied computing table of contents

Fortaleza, Ceara, Brazil

SESSION: Object-oriented programming languages and systems table of contents

Pages 184-188

Year of Publication: 2008

ISBN:978-1-59593-753-7

Authors

Francesco Logozzo	Microsoft Research
Manuel Fähndrich	Microsoft Research

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 35, Citation Count: 2

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1363686.1363736 What is a DOI?

ABSTRACT

We introduce Pentagons (Pntg), a weakly relational numerical abstract domain useful for the validation of array accesses in byte-code and intermediate languages (IL). This abstract domain captures properties of the form of x ε [a, b]∧x < y. It is more precise than the well known Interval domain, but it is less precise than the Octagon domain.

The goal of Pntg is to be a lightweight numerical domain useful for adaptive static analysis, where Pntg is used to quickly prove the safety of most array accesses, restricting the use of more precise (but also more expensive) domains to only a small fraction of the code.

We implemented the Pntg abstract domain in Clousot, a generic abstract interpreter for .NET assemblies. Using it, we were able to validate 83% of array accesses in the core runtime library mscorlib.dll in less than 8 minutes.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. Widening operators for weakly-relational numeric abstractions. In SAS'05. Springer-Verlag, Sept. 2005.
	2	Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
	3	P. Cousot. Verification by abstract interpretation. In Verification: Theory and Practice. Springer-Verlag, 2003.
	4	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	5	Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
	6	Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
	7	ECMA. Standard ECMA-335, Common Language Infrastructure (CLI). http://www.ecma-international.org/-publications/standards/ecma-335.htm, Ecma International, 2006.
	8	F. Logozzo. Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of Java classes. In VMCAI'07. Springer-Verlag, Jan. 2007.
	9	A. Miné. The octagon abstract domain. In WCRE 2001. IEEE Computer Society, Oct. 2001.
	10	J. Navas, E. Mera, P. López-García, and M. V. Hermenegildo. User-definable resource bounds analysis for logic programs. In ICLP'07. Springer-Verlag, Sept. 2007.
	11	A. Simon, A. King, and J. M. Howe. Two variables per linear inequality as an abstract domain. In LOPSTR'02. Springer-Verlag, 2002.
	12	Arnaud Venet, Nonuniform Alias Analysis of Recursive Data Structures and Arrays, Proceedings of the 9th International Symposium on Static Analysis, p.36-51, September 17-20, 2002
	13	Arnaud Venet , Guillaume Brat, Precise and efficient static array bound checking for large embedded C programs, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

CITED BY 2

	Pietro Ferrara , Francesco Logozzo , Manuel Fähndrich, Safer unsafe code for .NET, ACM SIGPLAN Notices, v.43 n.10, September 2008
	Corneliu Popeea , Dana N. Xu , Wei-Ngan Chin, A practical and precise inference and specializer for array bound checks elimination, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA