Abstract
While the use of pointers can be minimized by language mechanisms for data abstraction, alias avoidance and control, and disciplined software development techniques, ultimately, any verifying compiler effort must be able to verify code that makes use of them. Additionally, in order to scale, the verification machinery of such a compiler must use specifications to reason about components. This paper follows a natural question that arises from combining these ideas: can the general machinery of specification-based component verification also be used to verify code that uses instances of types that are more traditionally built-in, such as arrays and pointers? This paper answers the question in the affirmative by presenting a Location_Linking_Template, a concept that captures pointer behavior, and uses it to verify the code of a simple data abstraction realized using pointers. In this deployment, pointers have a specification like any other component. We also note that the concept can be extended and realized so that different systems can plug in alternative implementations to give programmers the flexibility to choose, e.g., manual memory management or automatic garbage collection depending on their performance concerns.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Banerjee, A., Naumann, D.A.: State Based Ownership, Reentrance, and Encapsulation. In: Gao, X.-X. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 387–411. Springer, Heidelberg (2005)
Böhme, S., Moskal, M.: Heaps and Data Structures: A Challenge for Automated Provers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 177–191. Springer, Heidelberg (2011), http://dx.doi.org/10.1007/978-3-642-22438-6_15
Harms, D.E., Weide, B.W.: Copying and swapping: Influences on the design of reusable software components. IEEE Trans. Softw. Eng. 17, 424–435 (1991), http://dl.acm.org/citation.cfm?id=114769.114773
Harton, H.: Mechanical and Modular Verification Condition Generation for Object-Based Software. Phd dissertation. Clemson University, School of Computing (December 2011)
Hatcliff, J., Leavens, G.T., Rustan, K., Leino, M., Müller, P., Parkinson, M.: Behavioral interface specification languages (2009), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.723
Hehner, E.C.R.: Formalization of time and space. Formal Aspects of Computing 10, 290–306 (1998), http://dx.doi.org/10.1007/s001650050017
Hoare, C.A.R.: Recursive data structures. In: Hoare, C.A.R., Jones, C.B. (eds.) Essays in Computing Science. Prentice-Hall, New York (1989)
Hollingsworth, J.E., Blankenship, L., Weide, B.W.: Experience report: using RESOLVE/C++ for commercial software. In: Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering: Twenty-First Century Applications, SIGSOFT 2000/FSE-8, pp. 11–19. ACM, New York (2000), http://doi.acm.org/10.1145/355045.355048
Jones, C.B.: Systematic software development using VDM. Prentice Hall International (UK) Ltd., Hertfordshire (1986)
Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing without Restrictions. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)
Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M.A., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Weiß, B.: The 1st Verified Software Competition: Experience Report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154–168. Springer, Heidelberg (2011)
Kulczycki, G.: Direct Reasoning. Phd dissertation. Clemson University, School of Computing (January 2004)
Kulczycki, G., Sitaraman, M., Roche, K., Yasmin, N.: Formal specification. In: Wah, B.W. (ed.) Wiley Encyclopedia of Computer Science and Engineering. John Wiley & Sons, Inc. (2008)
Kulczycki, G., Smith, H., Harton, H., Sitaraman, M., Ogden, W.F., Hollingsworth, J.E.: Technical report RSRG-11-04, The Location Linking Concept: A Basis for Verification of Code Using Pointers (September 2011), http://www.cs.clemson.edu/group/resolve/reports.html
Lahiri, S., Qadeer, S.: Back to the future: revisiting precise program verification using smt solvers. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 171–182. ACM, New York (2008), http://doi.acm.org/10.1145/1328438.1328461
Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall, Inc., Upper Saddle River (1988)
Meyer, B.: On to components. Computer 32, 139–140 (1999)
Noble, J., Vitek, J., Potter, J.: Flexible Alias Protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158–185. Springer, Heidelberg (1998)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, pp. 55–74. IEEE Computer Society, Washington, DC, USA (2002), http://dl.acm.org/citation.cfm?id=645683.664578
Sitaraman, M., Weide, B.: Component-based software using resolve. SIGSOFT Softw. Eng. Notes 19, 21–22 (1994), http://doi.acm.org/10.1145/190679.199221
Sitaraman, M., Adcock, B., Avigad, J., Bronish, D., Bucci, P., Frazier, D., Friedman, H., Harton, H., Heym, W., Kirschenbaum, J., Krone, J., Smith, H., Weide, B.: Building a push-button resolve verifier: Progress and challenges. Formal Aspects of Computing 23, 607–626 (2011), http://dx.doi.org/10.1007/s00165-010-0154-3
Sitaraman, M., Atkinson, S., Kulczycki, G., Weide, B.W., Long, T.J., Bucci, P., Heym, W.D., Pike, S.M., Hollingsworth, J.E.: Reasoning about Software-Component Behavior. In: Frakes, W.B. (ed.) ICSR 2000. LNCS, vol. 1844, pp. 266–283. Springer, Heidelberg (2000)
Sitaraman, M., Kulczycki, G., Krone, J., Ogden, W.F., Reddy, A.L.N.: Performance specification of software components. In: SSR, pp. 3–10 (2001)
Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall, Inc., Upper Saddle River (1989)
Wies, T., Muñiz, M., Kuncak, V.: An Efficient Decision Procedure for Imperative Tree Data Structures. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 476–491. Springer, Heidelberg (2011), http://dl.acm.org/citation.cfm?id=2032266.2032302
Wing, J.M.: A specifier’s introduction to formal methods. Computer 23, 8–23 (1990), http://dl.acm.org/citation.cfm?id=102815.102816
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kulczycki, G., Smith, H., Harton, H., Sitaraman, M., Ogden, W.F., Hollingsworth, J.E. (2012). The Location Linking Concept: A Basis for Verification of Code Using Pointers. In: Joshi, R., Müller, P., Podelski, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2012. Lecture Notes in Computer Science, vol 7152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27705-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-27705-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27704-7
Online ISBN: 978-3-642-27705-4
eBook Packages: Computer ScienceComputer Science (R0)