Article

A specification-based approach to reasoning about pointers

Authors:

Gregory Kulczycki,

Murali Sitaraman,

Bruce W. Weide,

Atanas RountevAuthors Info & Claims

SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems

Pages 7 - es

https://doi.org/10.1145/1123058.1123066

Published: 05 September 2005 Publication History

Abstract

This paper explains how a uniform, specification-based approach to reasoning about component-based programs can be used to reason about programs that manipulate pointers. No special axioms, language semantics, global heap model, or proof rules for pointers are necessary. We show how this is possible by capturing pointers and operations that manipulate them in the specification of a software component. The proposed approach is mechanizable as long as programmers are able to understand mathematical specifications and write assertions, such as loop invariants. While some of the previous efforts in reasoning do not require such mathematical sophistication on the part of programmers, they are limited in the kinds of properties they can prove about programs that use pointers. We illustrate the idea using a "Splice" operation for linked lists, which has been used previously to explain other analysis techniques. Not only can the proposed approach be used to establish shape properties given lightweight specifications, but also it can be used to establish total correctness given more complete specifications.

References

[1]

Abadi, M. and Leino, K. R. M. A logic of object-oriented programs. In M. Bidoit and M. Dauchet, editors, TAPSOFT '97: Theory and Practice of Software Development, 7th Internation Joint Conference, pages 682--696. Springer-Verlag, New York, 1997.]]

Digital Library

[2]

Barnett, M., Leino, K. R. M., and Schulte, W. The Spec# programming system: An overview. In CASSIS 2004, LNCS vol. 3362, Springer, 2004.]]

[3]

Borgida, A., Mylopoulos, J., and Reiter, R. ... and nothing else changes?: The frame problem in procedure specifications. In Proceedings of the 15th International Conference on Software Engineering. IEEE Computer Society Press, pages 303--314, 1993.]]

Digital Library

[4]

Cheon, Y., Leavens, G. T., Sitaraman, M., and Edwards, S. Model variables: Cleanly supporting abstraction in design by contract. Software, Practice, and Experience, 35 (6), pages 583--599, 2005.]]

Digital Library

[5]

Clarke, D. G., Potter, J. M., and Noble, J. Ownership types for flexible alias protection. In Proceedings OOPSLA '98, pages 48--64, 1998.]]

Digital Library

[6]

Hackett, B. and Rugina, R. Region-based shape analysis with tracked locations. In Proceedings POPL '05, January 2005.]]

Digital Library

[7]

Heym, W. Computer Program Verification: Improvements for Human Reasoning. Ph.D. thesis, The Ohio State University, 1995.]]

Digital Library

[8]

Hogg, J., Lea, D., Wills, A., deChampeaux, D., and Holt, R. The Geneva Convention on the treatment of object aliasing. OOPS Messenger, 3(2):11--16, 1992.]]

Digital Library

[9]

Jensen, J. L., Jorgensen, M. E., Klarlund, N., and Schwartzbach, M. I. Automatic verification of pointer programs using monadic second-order logic. In Proceedings SIGPLAN Conference on Programming Language Design and Implementation, 1997.]]

Digital Library

[10]

Krone, J. The Role of Verification in Software Reusability. Ph.D. thesis, The Ohio State University, 1988.]]

Digital Library

[11]

Krone, J., Ogden, W. F., and Sitaraman, M. Modular verification of performance correctness. In OOPSLA 2001 SAVCBS Workshop Proceedings, 2001. http://www.cs.iastate.edu/~leavens/SAVCBS/papers-2001/index.html.]]

[12]

Kulczycki, G., Sitaraman, M., Ogden, W. F., and Hollingsworth, J. E. Component Technology for Pointers: Why and How, Technical Report RSRG-03-03, Clemson University, Clemson, SC. 2003. http://www.cs.clemson.edu/~resolve/reports/RSRG-03-03.pdf]]

[13]

Leavens, G. T., Cheon, Y., Clifton, C., Ruby, C., and Cok. D. R. How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming, vol. 55, pages 185--205, Elsevier, 2005.]]

Digital Library

[14]

Leino, K. R. M. Data groups: specifying the modification of extended state. In Proceedings OOPSLA '98, pages 144--153, 1998.]]

Digital Library

[15]

Leino, K. R. M., Nelson, G., and Saxe, J. B. ESC/Java User's Manual, Technical Note 2000-002, Compaq Systems Research Center, October 2000.]]

[16]

Meyers, S. More Effective C++. Addison-Wesley, 1995.]]

[17]

Møller, A. and Schwartzbach, M. I. The pointer assertion logic engine. In ACM SIGPLAN Notices, 36(5), pages 221--231, May 2001.]]

Digital Library

[18]

Müller, P. and Poetzsch-Heffter, A. Modular specification and verification techniques for object-oriented software components. In Foundations of Component-Based Systems, G. T. Leavens and M. Sitaraman, editors, Cambridge University Press, Cambridge, United Kingdom, 2000.]]

Digital Library

[19]

Noble, J., Vitek, J., and Potter, J. Flexible alias protection. ECOOP '98. Lecture Notes in Computer Science, vol. 1445, pp. 158--185, 1998.]]

Digital Library

[20]

O'Hearn, P., Reynolds, J., and Yang, H. Local reasoning about programs that alter data structures. Lecture Notes in Computer Science, 2142:1--19, 2001.]]

Digital Library

[21]

Pike, S. M., Weide, B. W., and Hollingsworth, J. E. Checkmate: concerning C++ dynamic memory errors with checked pointers. In Proceedings of the 31st SIGCSE Technical Symposium on Computer Science Education. ACM Press, March 2000.]]

Digital Library

[22]

Sagiv, M., Reps, T., and Wilhelm, R. Parametric shape analysis via 3-valued logic. In ACM Transactions on Programming Languages and Systems, 24(3), pp. 217--298, 2002.]]

Digital Library

[23]

Sitaraman, M. and Weide, B. W. Component-based software using RESOLVE. ACM Software Engineering Notes, 19(4), pp. 21--67, 1994.]]

Digital Library

[24]

Sitaraman, M. Impact of performance considerations on formal specification design. Formal Aspects of Computing, 8(6):716--736, 1996.]]

[25]

Sitaraman, M., Atkinson, S., Kulczycki, G., Weide, B. W. Long, T. J., Bucci, P., Heym, W., Pike, S., and Hollingsworth, J. E. Reasoning about software-component behavior. In Proceedings of the 6th International Conference on Software Reuse, pages 266--283. Springer-Verlag, 2000.]]

Digital Library

[26]

Sitaraman, M., Gandi, D. P., Kuechlin, W., Sinz, C., and Weide, B. W. DEET for Component-Based Software, In Proceedings FSE Workshop on Specification and Verification of Component-Based Systems, October 2004.]]

[27]

Steensgaard, B. Points-to analysis in almost linear time. In Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages, January 1996.]]

Digital Library

[28]

Vaziri, M. and Jackson, D. Checking heap-manipulating procedures with a constraint solver. TACAS '03, Warsaw, Poland, 2003.]]

[29]

Weide, B. W., and Heym, W. D. Specification and verification with references. In Proceedings OOPSLA Workshop on Specification and Verification of Component-Based Systems, October 2001.]]

[30]

Wilhelm, R., Sagiv, M., and Reps, T. Shape analysis. In Proceedings of the 2000 International Conference on Compiler Construction, Berlin, Germany, April 2000.]]

Digital Library

[31]

Wing, J. M. A specifier's introduction to formal methods. IEEE Computer, 23(9):8--24, 1990.]]

Digital Library

Cited By

Kulczycki GKeown HSitaraman MWeide B(2007)Abstracting Pointers for a Verifying Compiler31st IEEE Software Engineering Workshop (SEW 2007)10.1109/SEW.2007.89(204-213)Online publication date: Mar-2007
https://doi.org/10.1109/SEW.2007.89
Kulczycki GVasudeo J(2006)Simplifying reasoning about objects with TakoProceedings of the 2006 conference on Specification and verification of component-based systems10.1145/1181195.1181207(57-64)Online publication date: 10-Nov-2006
https://dl.acm.org/doi/10.1145/1181195.1181207
Sitaraman MAdcock BAvigad JBronish DBucci PFrazier DFriedman HHarton HHeym WKirschenbaum JKrone JSmith HWeide B(2011)Building a push-button RESOLVE verifier: Progress and challengesFormal Aspects of Computing10.1007/s00165-010-0154-323:5(607-626)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1007/s00165-010-0154-3

Recommendations

A specification-based approach to reasoning about pointers

This paper explains how a uniform, specification-based approach to reasoning about component-based programs can be used to reason about programs that manipulate pointers. No special axioms, language semantics, global heap model, or proof rules for ...
Symbolic range analysis of pointers
CGO '16: Proceedings of the 2016 International Symposium on Code Generation and Optimization

Alias analysis is one of the most fundamental techniques that compilers use to optimize languages with pointers. However, in spite of all the attention that this topic has received, the current state-of-the-art approaches inside compilers still face ...
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

SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems

September 2005

95 pages

ISBN:1595933719

DOI:10.1145/1123058

Program Chair:
Gary T. Leavens
Iowa State

ACM SIGSOFT Software Engineering Notes Volume 31, Issue 2
March 2006
193 pages
ISSN:0163-5948
DOI:10.1145/1118537
Issue’s Table of Contents

Copyright © 2005 Authors.

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Acceptance Rates

SAVCBS '05 Paper Acceptance Rate 15 of 15 submissions, 100%;

Overall Acceptance Rate 37 of 46 submissions, 80%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
194
Total Downloads

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

Reflects downloads up to 16 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kulczycki GKeown HSitaraman MWeide B(2007)Abstracting Pointers for a Verifying Compiler31st IEEE Software Engineering Workshop (SEW 2007)10.1109/SEW.2007.89(204-213)Online publication date: Mar-2007
https://doi.org/10.1109/SEW.2007.89
Kulczycki GVasudeo J(2006)Simplifying reasoning about objects with TakoProceedings of the 2006 conference on Specification and verification of component-based systems10.1145/1181195.1181207(57-64)Online publication date: 10-Nov-2006
https://dl.acm.org/doi/10.1145/1181195.1181207
Sitaraman MAdcock BAvigad JBronish DBucci PFrazier DFriedman HHarton HHeym WKirschenbaum JKrone JSmith HWeide B(2011)Building a push-button RESOLVE verifier: Progress and challengesFormal Aspects of Computing10.1007/s00165-010-0154-323:5(607-626)Online publication date: 1-Sep-2011
https://dl.acm.org/doi/10.1007/s00165-010-0154-3

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