{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T00:04:55Z","timestamp":1768349095055,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540377566","type":"print"},{"value":"9783540377580","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11823230_17","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T13:46:30Z","timestamp":1155822390000},"page":"261-279","source":"Crossref","is-referenced-by-count":34,"title":["Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Loginov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Bornat, R.: Proofs of pointer programs in Jape. available at: http:\/\/www.dcs.qmul.ac.uk\/richard\/pointers\/"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Construction, pp. 102\u2013126 (July 2000)","DOI":"10.1007\/10722010_8"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1093\/comjnl\/42.3.177","volume":"43","author":"R. Bornat","year":"1999","unstructured":"Bornat, R., Sufrin, B.: Animating formal proofs at the surface: The Jape proof calculator. The Computer Journal\u00a043, 177\u2013192 (1999)","journal-title":"The Computer Journal"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Hendren, L.: Parallelizing Programs with Recursive Data Structures. PhD thesis, Dept. of Computer Science, Cornell University (January 1990)","DOI":"10.1145\/318789.318812"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: Bi as an assertion language for mutable data structures. In: Symp. on Principles of Programming Languages, pp. 14\u201326 (January 2001)","DOI":"10.1145\/360204.375719"},{"key":"17_CR6","series-title":"Fundamental Algorithms","volume-title":"The Art of Computer Programming","author":"D. Knuth","year":"1973","unstructured":"Knuth, D.: The Art of Computer Programming. Fundamental Algorithms, vol.\u00a01. Addison-Wesley, Reading (1973)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-31987-0_10","volume-title":"Programming Languages and Systems","author":"O. Lee","year":"2005","unstructured":"Lee, O., Yang, H., Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 124\u2013140. Springer, Heidelberg (2005)"},{"key":"17_CR8","unstructured":"Lev-Ami, T., Immerman, N., Sagiv, M.: Fast and precise abstraction for shape analysis. In: Proc. Computer-Aided Verification (August 2006) (to appear)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Int. Symp. on Software Testing and Analysis, pp. 26\u201338 (August 2000)","DOI":"10.1145\/347324.348031"},{"issue":"2","key":"17_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0020-0190(73)90012-4","volume":"2","author":"G. Lindstrom","year":"1973","unstructured":"Lindstrom, G.: Scanning list structures without stacks or tag bits. Information Processing Letters\u00a02(2), 47\u201351 (1973)","journal-title":"Information Processing Letters"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/11513988_50","volume-title":"Computer Aided Verification","author":"A. Loginov","year":"2005","unstructured":"Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 519\u2013533. Springer, Heidelberg (2005)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-27864-1_20","volume-title":"Static Analysis","author":"R. Manevich","year":"2004","unstructured":"Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 265\u2013279. Springer, Heidelberg (2004)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction \u2013 CADE-19","author":"F. Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS, vol.\u00a02741, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"17_CR14","unstructured":"Morris, J.: Verification-oriented language design. Tech. Report TR-7, Computer Science Div., University of California\u2013Berkeley (December 1972)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-36575-3_26","volume-title":"Programming Languages and Systems","author":"T. Reps","year":"2003","unstructured":"Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol.\u00a02618, pp. 380\u2013398. Springer, Heidelberg (2003)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation Logic: A logic for shared mutable data structures. In: Symp. on Logic in Computer Science, pp. 55\u201374 (July 2002)","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"3","key":"17_CR17","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. on Programming Languages and Systems (TOPLAS)\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM Trans. on Programming Languages and Systems (TOPLAS)"},{"issue":"8","key":"17_CR18","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/363534.363554","volume":"10","author":"H. Schorr","year":"1967","unstructured":"Schorr, H., Waite, W.: An efficient machine independent procedure for garbage collection in various list structures. Communications of the ACM\u00a010(8), 501\u2013506 (1967)","journal-title":"Communications of the ACM"},{"key":"17_CR19","unstructured":"Suzuki, N.: Automatic Verification of Programs with Complex Data Structures. PhD thesis, Dept. of Computer Science, Stanford University (February 1976)"},{"key":"17_CR20","unstructured":"Topor, R.: The correctness of the Schorr-Waite list marking algorithm. Tech. Report MIP-R-104, School of Artificial Intelligence, University of Edinburgh (July 1974)"},{"key":"17_CR21","unstructured":"Yang, H.: Local Reasoning for Stateful Programs. PhD thesis, Dept. of Computer Science, University of Illinois, Urbana-Champaign (June 2001)"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Yelowitz, L., Duncan, A.: Abstractions, instantiations, and proofs of marking algorithms. In: Symp. on Artificial Intelligence and Programming Languages, pp. 13\u201321 (August 1977)","DOI":"10.1145\/800228.806927"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Reps, T., Sagiv, M., Wilhelm, R.: Logical characterizations of heap abstractions. ACM Transactions on Computational Logic (TOCL) (to appear)","DOI":"10.1145\/1182613.1182618"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11823230_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:17:02Z","timestamp":1605644222000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11823230_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540377566","9783540377580"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11823230_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}