Article

A framework for numeric analysis of array operations

Authors:

Mooly SagivAuthors Info & Claims

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 338 - 350

https://doi.org/10.1145/1040305.1040333

Published: 12 January 2005 Publication History

Abstract

Automatic discovery of relationships among values of array elements is a challenging problem due to the unbounded nature of arrays. We present a framework for analyzing array operations that is capable of capturing numeric properties of array elements.In particular, the analysis is able to establish that all array elements are initialized by an array-initialization loop, as well as to discover numeric constraints on the values of initialized elements.The analysis is based on the combination of canonical abstraction and summarizing numeric domains. We describe a prototype implementation of the analysis and discuss our experience with applying the prototype to several examples, including the verification of correctness of an insertion-sort procedure.

References

[1]

R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the parma polyhedra library. In Static Analysis Sym ., volume 2477, pages 213--229, 2002.

Digital Library

[2]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In The Essence of Computation: Complexity, Analysis, Transformation., pages 85--108. Springer-Verlag, 2002.

Digital Library

[3]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Symp. on Princ. of Prog. Lang., pages 238--252, New York, NY, 1977. ACM Press.

Digital Library

[4]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Symp. on Princ. of Prog. Lang., pages 269--282, New York, NY, 1979. ACM Press.

Digital Library

[5]

P. Cousot and N. Halbwachs. Automatic discovery of linear constraints among variables of a program. In Symp. on Princ. of Prog. Lang., 1978.

Digital Library

[6]

C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Symp. on Princ.of Prog. Lang., pages 191--202, 2002.

Digital Library

[7]

D. Gopan, F. DiMaio, N. Dor,T. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In Tools and Algorithms for the Construction and Analysis of Systems, pages 512--529, 2004.

[8]

N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157--185, 1997.

Digital Library

[9]

S. K. Lahiri and R. E. Bryant. Indexed predicate discovery fof unbounded system verification. In Int. Conf.on Computer Aided Verification, pages 135--147, 2004.

[10]

L. Lamport. A new approach to proving the correctness of multiprocess programs. Trans. on Prog. Lang. and Syst., 1(1):84--97, July 1979.

Digital Library

[11]

T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Static Analysis Symp.,pages 280--301, 2000.

Digital Library

[12]

R. Manevich,M. Sagiv,G. Ramalingam, and J. Field. Partially disjunctive heap abstraction. In Static Analysis Symp., pages 265--279, 2004.

[13]

F. Masdupuy. Array Indices Relational Semantic Analysis using Rational Cosets and Trapezoids. PhD thesis, Ecole Polytechnique, 1993.

[14]

A. Mine. The octagon abstract domain. In Proc. Eighth Working Conf. on Rev. Eng., pages 310--322, 2001.

Digital Library

[15]

A. Mine. A few graph-based relational numerical abstract domains. In Static Analysis Symp., pages 117--132, 2002.

Digital Library

[16]

G. Peterson. Myths about the mutual exclusion problem. Information Processing Letters, 12(3):115--116, June 1981.

[17]

T. Reps, M.S agiv, and A. Loginov. Finite differencing of logical formulas for static analysis. In Eurorean Symp. on Programming, pages 380--398, 2003.

Digital Library

[18]

T. Reps, M. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. In Verification, Model Checking, and Abstract Interpretation, pages 252--266, 2004.

[19]

M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst., 24(3):217--298, 2002.

Digital Library

[20]

P. Černý. Vérification pa interpétation abstraite de prédicats paramétriques. D.E.A. Report, Univ. Paris VII & ÉÉcole normale supérieure, September 2003.

[21]

G. Yorsh, T. Reps, and M. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In Tools and Algorithms for the Construction and Analysis of Systems, pages 530--545, 2004.

Cited By

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
Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Malík VSchrammel PVojnar T(2024)Template-Based Verification of Array-Manipulating ProgramsTaming the Infinities of Concurrency10.1007/978-3-031-56222-8_12(206-224)Online publication date: 20-Mar-2024
https://doi.org/10.1007/978-3-031-56222-8_12
Show More Cited By

Index Terms

A framework for numeric analysis of array operations
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

A framework for numeric analysis of array operations
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Automatic discovery of relationships among values of array elements is a challenging problem due to the unbounded nature of arrays. We present a framework for analyzing array operations that is capable of capturing numeric properties of array ...
Temporal property verification as a program analysis task

We describe a reduction from temporal property verification to a program analysis problem. First we present a proof system that, unlike the standard formulation, is more amenable to reasoning about infinite-state systems: disjunction is treated by ...
Shape predicates allow unbounded verification of linearizability using canonical abstraction
ACSC '14: Proceedings of the Thirty-Seventh Australasian Computer Science Conference - Volume 147

Canonical abstraction is a static analysis technique that represents states as 3-valued logical structures, and is able to construct finite representations of systems with infinite statespaces for verification. The granularity of the abstraction can be ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

402 pages

ISBN:158113830X

DOI:10.1145/1040305

General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

ACM SIGPLAN Notices Volume 40, Issue 1
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
391 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1047659
Issue’s Table of Contents

Copyright © 2005 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL05

Sponsor:

POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005

January 12 - 14, 2005

California, Long Beach, USA

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

150
Total Citations
View Citations
797
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)1

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

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
Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z
Malík VSchrammel PVojnar T(2024)Template-Based Verification of Array-Manipulating ProgramsTaming the Infinities of Concurrency10.1007/978-3-031-56222-8_12(206-224)Online publication date: 20-Mar-2024
https://doi.org/10.1007/978-3-031-56222-8_12
Utture APalsberg JChandra SBlincoe KTonella P(2023)From Leaks to Fixes: Automated Repairs for Resource Leak WarningsProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616267(159-171)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616267
Giet JRidoux FRival X(2023)A Product of Shape and Sequence AbstractionsStatic Analysis10.1007/978-3-031-44245-2_15(310-342)Online publication date: 24-Oct-2023
https://doi.org/10.1007/978-3-031-44245-2_15
Li PMeng W(2021)LChecker: Detecting Loose Comparison Bugs in PHPProceedings of the Web Conference 202110.1145/3442381.3449826(2721-2732)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3442381.3449826
Zhang QZhang YLi XWu B(2021)Discovering Properties about Arrays via Path Dependence Analysis2021 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE52547.2021.00022(55-62)Online publication date: Aug-2021
https://doi.org/10.1109/TASE52547.2021.00022
Du XYin LDong W(2021)Simplify Array Processing Loops for Efficient Program Verification2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE52982.2021.00049(401-411)Online publication date: Oct-2021
https://doi.org/10.1109/ISSRE52982.2021.00049
Braine JGonnord LMonniaux D(2021)Data Abstraction: A General Framework to Handle Program Verification of Data StructuresStatic Analysis10.1007/978-3-030-88806-0_11(215-235)Online publication date: 13-Oct-2021
https://doi.org/10.1007/978-3-030-88806-0_11
Zhang YRen LChen LXiong YCheung SXie TDevanbu PCohen MZimmermann T(2020)Detecting numerical bugs in neural network architecturesProceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3368089.3409720(826-837)Online publication date: 8-Nov-2020
https://dl.acm.org/doi/10.1145/3368089.3409720
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.

Figures

Tables

Media

View Table of Conten