More Web Proxy on the site http://driver.im/

research-article

Precise and compact modular procedure summaries for heap manipulating programs

Authors:

Mooly SagivAuthors Info & Claims

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 567 - 577

https://doi.org/10.1145/1993498.1993565

Published: 04 June 2011 Publication History

Abstract

We present a strictly bottom-up, summary-based, and precise heap analysis targeted for program verification that performs strong updates to heap locations at call sites. We first present a theory of heap decompositions that forms the basis of our approach; we then describe a full analysis algorithm that is fully symbolic and efficient. We demonstrate the precision and scalability of our approach for verification of real C and C++ programs.

References

[1]

Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the saturn project. In: PASTE, ACM (2007) 43--48

Digital Library

[2]

Bush, W., Pincus, J., Sielaff, D.: A static analyzer for finding dynamic programming errors. Software: Practice and Experience 30(7) (2000) 775--802

Digital Library

[3]

Reps, T.W., Sagiv, S., Wilhelm, R.: Static program analysis via 3-valued logic. In: CAV. Volume 3114., Springer (2004) 15--30

[4]

Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. weak updates. In: ESOP. (2010)

Digital Library

[5]

Landi, W., Ryder, B.G.: A safe approximate algorithm for interprocedural aliasing. SIGPLAN Not. 27(7) (1992) 235--248

Digital Library

[6]

Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for c programs. In: PLDI. (1995)

Digital Library

[7]

Chatterjee, R., Ryder, B., Landi, W.: Relevant context inference. In: POPL, ACM (1999) 133--146

Digital Library

[8]

Dillig, I., Dillig, T., Aiken, A.: Sound, complete and scalable path-sensitive analysis. In: PLDI, ACM (2008) 270--280

Digital Library

[9]

Whaley, J., Rinard, M.: Compositional pointer and escape analysis for Java programs. In: OOPSLA, ACM (1999) 187--206

Digital Library

[10]

Salcinau, A.: Pointer Analysis for Java Programs: Novel Techniques and Applications. PhD thesis, MIT (2006)

Digital Library

[11]

Calcagno, C., Distefano, D., O'Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. POPL (2009) 289--300

Digital Library

[12]

Gulavani, B., Chakraborty, S., Ramalingam, G., Nori, A.: Bottom-up shape analysis. SAS (2009) 188--204

Digital Library

[13]

Cousot, P., Cousot, R.: Modular static program analysis. In: CC. (2002) 159--178

Digital Library

[14]

Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. ESOP (2007) 253--267

Digital Library

[15]

Pnueli, M.: Two approaches to interprocedural data flow analysis. Program Flow Analysis: Theory and Applications (1981) 189--234

[16]

Yorsh, G., Yahav, E., Chandra, S.: Generating precise and concise procedure summaries. POPL 43(1) (2008) 221--234

Digital Library

[17]

Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: POPL. (1995) 49--61

Digital Library

[18]

Sagiv, S., Reps, T.W., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167(1&2) (1996) 131--170

Digital Library

Cited By

Yao PZhou JXiao XShi QWu RZhang C(2024)Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence AnalysisProceedings of the ACM on Programming Languages10.1145/36564008:PLDI(567-592)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656400
Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Wu RHe YHuang JWang CTang WShi QXiao XZhang CRoychoudhury APaiva AAbreu RStorey M(2024)LibAlchemy: A Two-Layer Persistent Summary Design for Taming Third-Party Libraries in Static Bug-Finding SystemsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639132(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639132
Show More Cited By

Index Terms

Precise and compact modular procedure summaries for heap manipulating programs

Recommendations

Precise and compact modular procedure summaries for heap manipulating programs
PLDI '11

We present a strictly bottom-up, summary-based, and precise heap analysis targeted for program verification that performs strong updates to heap locations at call sites. We first present a theory of heap decompositions that forms the basis of our ...
Flexible pointer analysis using assign-fetch graphs
SAC '08: Proceedings of the 2008 ACM symposium on Applied computing

We propose a new abstraction for pointer analysis that represents reads and writes to memory instead of traditional points-to relations. Compared to points-to graphs, our Assign-Fetch Graph (AFG) leads to concise procedure summaries that can be used in ...
Precise Call Graphs for C Programs with Function Pointers

The use of pointers presents serious problems for software productivity tools for software understanding, restructuring, and testing. Pointers enable indirect memory accesses through pointer dereferences, as well as indirect procedure calls (e.g., ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2011

668 pages

ISBN:9781450306638

DOI:10.1145/1993498

General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

ACM SIGPLAN Notices Volume 46, Issue 6
PLDI '11
June 2011
652 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1993316
Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '11

Sponsor:

SIGPLAN

PLDI '11: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 4 - 8, 2011

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

77
Total Citations
View Citations
639
Total Downloads

Downloads (Last 12 months)30
Downloads (Last 6 weeks)4

Reflects downloads up to 20 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yao PZhou JXiao XShi QWu RZhang C(2024)Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence AnalysisProceedings of the ACM on Programming Languages10.1145/36564008:PLDI(567-592)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656400
Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Wu RHe YHuang JWang CTang WShi QXiao XZhang CRoychoudhury APaiva AAbreu RStorey M(2024)LibAlchemy: A Two-Layer Persistent Summary Design for Taming Third-Party Libraries in Static Bug-Finding SystemsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639132(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639132
Sun YWang CFan GShi QZhang X(2024)Fast and Precise Static Null Exception Analysis With Synergistic PreprocessingIEEE Transactions on Software Engineering10.1109/TSE.2024.346655150:11(3022-3036)Online publication date: 1-Nov-2024
https://dl.acm.org/doi/10.1109/TSE.2024.3466551
Sun CMa YZeng DTan GMa SWu Y(2023)μDep: Mutation-Based Dependency Generation for Precise Taint Analysis on Android Native CodeIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2022.315569320:2(1461-1475)Online publication date: 1-Mar-2023
https://doi.org/10.1109/TDSC.2022.3155693
Keshani MGousios GProksch S(2023)Frankenstein: fast and lightweight call graph generation for software buildsEmpirical Software Engineering10.1007/s10664-023-10388-729:1Online publication date: 16-Nov-2023
https://dl.acm.org/doi/10.1007/s10664-023-10388-7
Crichton WPatrignani MAgrawala MHanrahan PJhala RDillig I(2022)Modular information flow through ownershipProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523445(1-14)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523445
Cai YYao PZhang CFreund SYahav E(2021)Canary: practical static detection of inter-thread value-flow bugsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454099(1126-1140)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454099
Shi QYao PWu RZhang CFreund SYahav E(2021)Path-sensitive sparse analysis without path conditionsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454086(930-943)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454086
Illous HLemerre MRival X(2021)A relational shape abstract domainFormal Methods in System Design10.1007/s10703-021-00366-4Online publication date: 24-Apr-2021
https://doi.org/10.1007/s10703-021-00366-4
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents