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

Article

Arithmetic strengthening for shape analysis

Authors:

Stephen Magill,

Byron CookAuthors Info & Claims

SAS'07: Proceedings of the 14th international conference on Static Analysis

Pages 419 - 436

Published: 22 August 2007 Publication History

Abstract

Shape analyses are often imprecise in their numerical reasoning, whereas numerical static analyses are often largely unaware of the shape of a program's heap. In this paper we propose a lazy method of combining a shape analysis based on separation logic with an arbitrary arithmetic analysis. When potentially spurious counterexamples are reported by our shape analysis, the method constructs a purely arithmetic program whose traces over-approximate the set of counterexample traces. It then uses this arithmetic program together with the arithmetic analysis to construct a refinement for the shape analysis. Our method is aimed at proving properties that require comprehensive reasoning about heaps together with more targeted arithmetic reasoning. Given a sufficient precondition, our technique can automatically prove memory safety of programs whose error-free operation depends on a combination of shape, size, and integer invariants. We have implemented our algorithm and tested it on a number of common list routines using a variety of arithmetic analysis tools for refinement.

References

[1]

Armando, A., Benerecetti, M., Mantovani, J.: Model checking linear programs with arrays. Electr. Notes Theor. Comput. Sci. 144(3), 79-94 (2006)

Digital Library

[2]

Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI'2001: Programming Language Design and Implementation, vol. 36, pp. 203-213. ACM Press, New York (2001)

Digital Library

[3]

Berdine, J., Calcagno, C., O'Hearn, P.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, Springer, Heidelberg (2005)

Digital Library

[4]

Berdine, J., Cook, B., Distefano, D., O'Hearn, P.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R. B. (eds.) CAV 2006. LNCS, vol. 4144, Springer, Heidelberg (2006)

Digital Library

[5]

Beyer, D., Henzinger, T., Majumdar, R., Rybalchenko, A.: Path invarints. In: PLDI (2007)

Digital Library

[6]

Beyer, D., Henzinger, T. A., Théoduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R. B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 532-546. Springer, Heidelberg (2006)

Digital Library

[7]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI'2003: Programming Language Design and Implementation, pp. 196-207. ACM Press, New York (2003)

Digital Library

[8]

Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R. B. (eds.) CAV 2006. LNCS, vol. 4144, Springer, Heidelberg (2006)

Digital Library

[9]

Calcagno, C., Distefano, D., O'Hearn, P., Yang, H.: Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, Springer, Heidelberg (2006)

Digital Library

[10]

Choi, Y., Rayadurgam, S., Heimdahl, M. P.: Automatic abstraction for model checking software systems with interrelated numeric constraints. In: Proc. of ESEC/FSE, pp. 164-174. ACM Press, New York (2001)

Digital Library

[11]

Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL'1979: Principles of Programming Languages, pp. 269-282. ACM Press, New York (1979)

Digital Library

[12]

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978)

Digital Library

[13]

Distefano, D., O'Hearn, P. W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, Springer, Heidelberg (2006)

Digital Library

[14]

Dor, N., Rodeh, M., Sagiv, M.: Cssv: towards a realistic tool for statically detecting all buffer overflows in c. In: PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, New York, Ny, USA, pp. 155-167. ACM Press, New York, USA (2003)

Digital Library

[15]

Flanagan, C.: Software model checking via iterative abstraction refinement of constraint logic queries. In: CP+CV'04 (2004)

[16]

Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, Springer, Heidelberg (2004)

[17]

Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 279-293. Springer, Heidelberg (2006)

Digital Library

[18]

Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Ball, T. (ed.) ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI 2006, ACM Press, New York (2006)

Digital Library

[19]

Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL'2002: Principles of Programming Languages, pp. 58-70. ACM Press, New York (2002)

Digital Library

[20]

Kroening, D., Weissenbacher, G.: Counterexamples with loops for predicate abstraction. In: Ball, T., Jones, R. B. (eds.) CAV 2006. LNCS, vol. 4144, Springer, Heidelberg (2006)

Digital Library

[21]

Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. Technical Report CMU-CS-07-135, Carnegie Mellon University (2007)

[22]

Magill, S., Nanevski, A., Clarke, E., Lee, P.: Inferring invariants in separation logic for imperative list-processing programs. In: SPACE 2006: Third Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (2006)

[23]

Miné, A.: The Octagon abstract domain. Higher-Order and Symbolic Computation (to appear)

[24]

Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, Springer, Heidelberg (2006)

Digital Library

[25]

Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55-74. IEEE Computer Society Press, Los Alamitos (2002)

Digital Library

[26]

Rugina, R.: Quantitative shape analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)

[27]

Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: TOPLAS (2002)

Digital Library

[28]

Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M. V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, Springer, Heidelberg (2002)

Digital Library

[29]

Zhang, T., Sipma, H. B., Manna, Z.: Decision procedures for queues with integer constraints. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 225-237. Springer, Heidelberg (2005)

Digital Library

Cited By

Roe KSmith STalpin JDerler PSchneider K(2017)Using the coq theorem prover to verify complex data structure invariantsProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3127041.3127061(118-121)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3127041.3127061
Ferrara P(2016)A generic framework for heap and value analyses of object-oriented programming languagesTheoretical Computer Science10.1016/j.tcs.2016.04.001631:C(43-72)Online publication date: 6-Jun-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.04.001
Cook BKhlaaf HPiterman NJobstmann B(2014)Faster Temporal Reasoning for Infinite-State ProgramsProceedings of the 14th Conference on Formal Methods in Computer-Aided Design10.5555/2682923.2682942(75-82)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.5555/2682923.2682942
Show More Cited By

Arithmetic strengthening for shape analysis
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Formal Design of Arithmetic Circuits Based on Arithmetic Description Language

This paper presents a formal design of arithmetic circuits using an arithmetic description language called ARITH. The key idea in ARITH is to describe arithmetic algorithms directly with high-level mathematical objects (i.e., number representation ...
High speed computer arithmetic architectures
Options for Denormal Representation in Logarithmic Arithmetic
Abstract
Economical hardware often uses a FiXed-point Number System (FXNS), whose constant absolute precision is acceptable for many signal-processing algorithms. The almost-constant relative precision of the more expensive Floating-Point (FP) number ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SAS'07: Proceedings of the 14th international conference on Static Analysis

August 2007

467 pages

ISBN:3540740600

Editors:
Hanne Riis Nielson
Technical University of Denmark, Informatics and Mathematical Modelling, Kongens Lyngby, Denmark
,
Gilberto Filé
University of Padova, Department of Pure and Applied Mathematics, Padova, Italy

Sponsors

IMM Graduate School: IMM Graduate School
IBM Denmark: IBM Denmark

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 22 August 2007

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

39
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Roe KSmith STalpin JDerler PSchneider K(2017)Using the coq theorem prover to verify complex data structure invariantsProceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3127041.3127061(118-121)Online publication date: 29-Sep-2017
https://dl.acm.org/doi/10.1145/3127041.3127061
Ferrara P(2016)A generic framework for heap and value analyses of object-oriented programming languagesTheoretical Computer Science10.1016/j.tcs.2016.04.001631:C(43-72)Online publication date: 6-Jun-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.04.001
Cook BKhlaaf HPiterman NJobstmann B(2014)Faster Temporal Reasoning for Infinite-State ProgramsProceedings of the 14th Conference on Formal Methods in Computer-Aided Design10.5555/2682923.2682942(75-82)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.5555/2682923.2682942
Thakur ABreck JReps TRungta NTkachuk O(2014)Satisfiability modulo abstraction for separation logic with linked listsProceedings of the 2014 International SPIN Symposium on Model Checking of Software10.1145/2632362.2632376(58-67)Online publication date: 21-Jul-2014
https://dl.acm.org/doi/10.1145/2632362.2632376
Lee WPark S(2014)A proof system for separation logic with magic wandACM SIGPLAN Notices10.1145/2578855.253587149:1(477-490)Online publication date: 8-Jan-2014
https://dl.acm.org/doi/10.1145/2578855.2535871
Lee WPark SJagannathan SSewell P(2014)A proof system for separation logic with magic wandProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2535838.2535871(477-490)Online publication date: 11-Jan-2014
https://dl.acm.org/doi/10.1145/2535838.2535871
Ferrara P(2014)Generic Combination of Heap and Value Analyses in Abstract InterpretationProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_17(302-321)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_17
Chen LLi RWu XWang JShin SMaldonado J(2013)Static analysis of list-manipulating programs via bit-vectors and numerical abstractionsProceedings of the 28th Annual ACM Symposium on Applied Computing10.1145/2480362.2480589(1204-1210)Online publication date: 18-Mar-2013
https://dl.acm.org/doi/10.1145/2480362.2480589
Park JSeo JPark S(2013)A theorem prover for Boolean BIACM SIGPLAN Notices10.1145/2480359.242909548:1(219-232)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429095
Park JSeo JPark SGiacobazzi RCousot R(2013)A theorem prover for Boolean BIProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2429069.2429095(219-232)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2429069.2429095
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents