{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:30:49Z","timestamp":1742956249949,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642277047"},{"type":"electronic","value":"9783642277054"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_4","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T17:18:06Z","timestamp":1327511886000},"page":"34-49","source":"Crossref","is-referenced-by-count":6,"title":["The Location Linking Concept: A Basis for Verification of Code Using Pointers"],"prefix":"10.1007","author":[{"given":"Gregory","family":"Kulczycki","sequence":"first","affiliation":[]},{"given":"Hampton","family":"Smith","sequence":"additional","affiliation":[]},{"given":"Heather","family":"Harton","sequence":"additional","affiliation":[]},{"given":"Murali","family":"Sitaraman","sequence":"additional","affiliation":[]},{"given":"William F.","family":"Ogden","sequence":"additional","affiliation":[]},{"given":"Joseph E.","family":"Hollingsworth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/11531142_17","volume-title":"ECOOP 2005 - Object-Oriented Programming","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: State Based Ownership, Reentrance, and Encapsulation. In: Gao, X.-X. (ed.) ECOOP 2005. LNCS, vol.\u00a03586, pp. 387\u2013411. Springer, Heidelberg (2005)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-22438-6_15","volume-title":"Automated Deduction \u2013 CADE-23","author":"S. B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Moskal, M.: Heaps and Data Structures: A Challenge for Automated Provers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 177\u2013191. Springer, Heidelberg (2011), http:\/\/dx.doi.org\/10.1007\/978-3-642-22438-6_15"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1109\/32.90445","volume":"17","author":"D.E. Harms","year":"1991","unstructured":"Harms, D.E., Weide, B.W.: Copying and swapping: Influences on the design of reusable software components. IEEE Trans. Softw. Eng.\u00a017, 424\u2013435 (1991), http:\/\/dl.acm.org\/citation.cfm?id=114769.114773","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR4","unstructured":"Harton, H.: Mechanical and Modular Verification Condition Generation for Object-Based Software. Phd dissertation. Clemson University, School of Computing (December 2011)"},{"key":"4_CR5","unstructured":"Hatcliff, J., Leavens, G.T., Rustan, K., Leino, M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages (2009), http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.150.723"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/s001650050017","volume":"10","author":"E.C.R. Hehner","year":"1998","unstructured":"Hehner, E.C.R.: Formalization of time and space. Formal Aspects of Computing\u00a010, 290\u2013306 (1998), http:\/\/dx.doi.org\/10.1007\/s001650050017","journal-title":"Formal Aspects of Computing"},{"key":"4_CR7","volume-title":"Essays in Computing Science","author":"C.A.R. Hoare","year":"1989","unstructured":"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)"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/355045.355048","volume-title":"Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering: Twenty-First Century Applications, SIGSOFT 2000\/FSE-8","author":"J.E. Hollingsworth","year":"2000","unstructured":"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\u201319. ACM, New York (2000), http:\/\/doi.acm.org\/10.1145\/355045.355048"},{"key":"4_CR9","volume-title":"Systematic software development using VDM.","author":"C.B. Jones","year":"1986","unstructured":"Jones, C.B.: Systematic software development using VDM. Prentice Hall International (UK) Ltd., Hertfordshire (1986)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"I.T. Kassios","year":"2006","unstructured":"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.\u00a04085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V. Klebanov","year":"2011","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, 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\u00df, B.: The 1st Verified Software Competition: Experience Report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 154\u2013168. Springer, Heidelberg (2011)"},{"key":"4_CR12","unstructured":"Kulczycki, G.: Direct Reasoning. Phd dissertation. Clemson University, School of Computing (January 2004)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1002\/9780470050118.ecse161"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-642-27705-4_4"},{"key":"4_CR15","first-page":"171","volume-title":"Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008","author":"S. Lahiri","year":"2008","unstructured":"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\u2013182. ACM, New York (2008), http:\/\/doi.acm.org\/10.1145\/1328438.1328461"},{"key":"4_CR16","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall, Inc., Upper Saddle River (1988)","edition":"1"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/2.738312","volume":"32","author":"B. Meyer","year":"1999","unstructured":"Meyer, B.: On to components. Computer\u00a032, 139\u2013140 (1999)","journal-title":"Computer"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP \u201998 - Object-Oriented Programming","author":"J. Noble","year":"1998","unstructured":"Noble, J., Vitek, J., Potter, J.: Flexible Alias Protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol.\u00a01445, pp. 158\u2013185. Springer, Heidelberg (1998)"},{"key":"4_CR19","first-page":"55","volume-title":"Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"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\u201374. IEEE Computer Society, Washington, DC, USA (2002), http:\/\/dl.acm.org\/citation.cfm?id=645683.664578"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/190679.199221","volume":"19","author":"M. Sitaraman","year":"1994","unstructured":"Sitaraman, M., Weide, B.: Component-based software using resolve. SIGSOFT Softw. Eng. Notes\u00a019, 21\u201322 (1994), http:\/\/doi.acm.org\/10.1145\/190679.199221","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/s00165-010-0154-3","volume":"23","author":"M. Sitaraman","year":"2011","unstructured":"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\u00a023, 607\u2013626 (2011), http:\/\/dx.doi.org\/10.1007\/s00165-010-0154-3","journal-title":"Formal Aspects of Computing"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-44995-9_16","volume-title":"Software Reuse: Advances in Software Reusability","author":"M. Sitaraman","year":"2000","unstructured":"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.\u00a01844, pp. 266\u2013283. Springer, Heidelberg (2000)"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Sitaraman, M., Kulczycki, G., Krone, J., Ogden, W.F., Reddy, A.L.N.: Performance specification of software components. In: SSR, pp. 3\u201310 (2001)","DOI":"10.1145\/379377.375223"},{"key":"4_CR24","volume-title":"The Z notation: a reference manual","author":"J.M. Spivey","year":"1989","unstructured":"Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall, Inc., Upper Saddle River (1989)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-22438-6_36","volume-title":"Automated Deduction \u2013 CADE-23","author":"T. Wies","year":"2011","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An Efficient Decision Procedure for Imperative Tree Data Structures. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 476\u2013491. Springer, Heidelberg (2011), http:\/\/dl.acm.org\/citation.cfm?id=2032266.2032302"},{"key":"4_CR26","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"J.M. Wing","year":"1990","unstructured":"Wing, J.M.: A specifier\u2019s introduction to formal methods. Computer\u00a023, 8\u201323 (1990), http:\/\/dl.acm.org\/citation.cfm?id=102815.102816","journal-title":"Computer"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,27]],"date-time":"2021-12-27T00:44:54Z","timestamp":1640565894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}