{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T16:32:19Z","timestamp":1693845139634},"reference-count":32,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1988,4,1]],"date-time":"1988-04-01T00:00:00Z","timestamp":575856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":9238,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[1988,4]]},"DOI":"10.1016\/0167-6423(88)90026-3","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T04:19:32Z","timestamp":1027657172000},"page":"177-210","source":"Crossref","is-referenced-by-count":13,"title":["Verification of programs that destructively manipulate data"],"prefix":"10.1016","volume":"10","author":[{"given":"Ian A.","family":"Mason","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0167-6423(88)90026-3_BIB1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1137\/0212047","article-title":"Varieties of if-then-else","volume":"12","author":"Bloom","year":"1983","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0167-6423(88)90026-3_BIB2","first-page":"23","article-title":"Some techniques for proving correctness of programs which alter data structures","volume":"7","author":"Burstall","year":"1972"},{"key":"10.1016\/0167-6423(88)90026-3_BIB3","series-title":"Proc. IFIP Congress","first-page":"308","article-title":"Program proving as hand simulation with a little induction","author":"Burstall","year":"1974"},{"issue":"1","key":"10.1016\/0167-6423(88)90026-3_BIB4","doi-asserted-by":"crossref","DOI":"10.1145\/321992.321996","article-title":"A transformation system for developing recursive programs","volume":"24","author":"Burstall","year":"1977","journal-title":"J. ACM"},{"issue":"3","key":"10.1016\/0167-6423(88)90026-3_BIB5","doi-asserted-by":"crossref","DOI":"10.1016\/0020-0190(80)90130-1","article-title":"The Schorr-Waite marking algorithm revisited","volume":"11","author":"Dershowitz","year":"1980","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/0167-6423(88)90026-3_BIB6","unstructured":"L.P. Deutsch, in: [13], p. 417."},{"key":"10.1016\/0167-6423(88)90026-3_BIB7","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0167-6423(86)90026-2","article-title":"Program derivation through transformations: The evolution of list-copying algorithms","volume":"6","author":"Van Diepen","year":"1986","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0167-6423(88)90026-3_BIB8","first-page":"19","article-title":"Assigning meanings to programs","volume":"19","author":"Floyd","year":"1967"},{"key":"10.1016\/0167-6423(88)90026-3_BIB9","article-title":"Computational uses of the manipulation of formal proofs","author":"Goad","year":"1980","journal-title":"Stanford Computer Science Report No. STAN-CS-80-819"},{"key":"10.1016\/0167-6423(88)90026-3_BIB10","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF00289068","article-title":"The Schorr-Waite graph marking algorithm","volume":"11","author":"Gries","year":"1979","journal-title":"Acta Informat."},{"key":"10.1016\/0167-6423(88)90026-3_BIB11","article-title":"On the axiomatization of if-then-else","author":"Guessarian","year":"1985","journal-title":"CSLI Report No. CSLI-85-20"},{"key":"10.1016\/0167-6423(88)90026-3_BIB12","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","article-title":"Proof of correctness of data representations","volume":"1","author":"Hoare","year":"1972","journal-title":"Acta Informat."},{"key":"10.1016\/0167-6423(88)90026-3_BIB13","volume":"Volume 1","author":"Knuth","year":"1968"},{"key":"10.1016\/0167-6423(88)90026-3_BIB14","series-title":"Ph.D. Thesis","article-title":"Correctness of programs manipulating data structures","author":"Kowaltowski","year":"1973"},{"key":"10.1016\/0167-6423(88)90026-3_BIB15","series-title":"Proc. 6th Annual ACM Symposium on Principles of Programming Languages","article-title":"The evolution of list-copying algorithms","author":"Lee","year":"1979"},{"key":"10.1016\/0167-6423(88)90026-3_BIB16","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1145\/359340.359353","article-title":"Is sometimes better than always? Intermittent assertions in proving program correctness","volume":"Volume 21","author":"Manna","year":"1977","journal-title":"Communications of the ACM"},{"key":"10.1016\/0167-6423(88)90026-3_BIB17","article-title":"The deductive synthesis of imerative LISP programs","author":"Manna","year":"1987","journal-title":"AAAI"},{"key":"10.1016\/0167-6423(88)90026-3_BIB18","article-title":"The Semantics of Destructive Lisp","volume":"5","author":"Mason","year":"1986"},{"key":"10.1016\/0167-6423(88)90026-3_BIB19","article-title":"Memories of S-expressions","author":"Mason","year":"1985","journal-title":"Stanford Computer Science Report No. STAN-CS-85-1057"},{"key":"10.1016\/0167-6423(88)90026-3_BIB20","article-title":"An algebraic definition of simulation between programs","author":"Milner","year":"1971","journal-title":"Stanford Computer Science Report No. STAN-CS-71-205"},{"key":"10.1016\/0167-6423(88)90026-3_BIB21","series-title":"Technical Report 7","article-title":"Verification-oriented language design","author":"Morris","year":"1972"},{"key":"10.1016\/0167-6423(88)90026-3_BIB22","article-title":"Reasoning about recursively defined data structures","author":"Oppen","year":"1978","journal-title":"Stanford AIM-314"},{"key":"10.1016\/0167-6423(88)90026-3_BIB23","series-title":"Covering functions","author":"Poupon","year":"1972"},{"key":"10.1016\/0167-6423(88)90026-3_BIB24","article-title":"Expression procedures and program derivation","author":"Scherlis","year":"1980","journal-title":"Stanford Computer Science Report No. STAN-CS-80-818"},{"key":"10.1016\/0167-6423(88)90026-3_BIB25","article-title":"First steps towards inferential programming","volume":"83","author":"Scherlis","year":"1983"},{"key":"10.1016\/0167-6423(88)90026-3_BIB26","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1145\/363534.363554","article-title":"An efficient machine-independent procedure for garbage collection in various list structures","volume":"10","author":"Schorr","year":"1987","journal-title":"Comm. ACM"},{"key":"10.1016\/0167-6423(88)90026-3_BIB27","series-title":"Ph.D. Thesis","article-title":"Automatic verification of programs with complex data structures","author":"Suzuki","year":"1976"},{"issue":"5","key":"10.1016\/0167-6423(88)90026-3_BIB28","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1145\/358506.358513","article-title":"Analysis of pointer rotation","volume":"25","author":"Suzuki","year":"1982","journal-title":"Comm. ACM"},{"key":"10.1016\/0167-6423(88)90026-3_BIB29","article-title":"The essence of RUM","author":"Talcott","year":"1985","journal-title":"Stanford Computer Science Report No. STAN-CS-85-1060"},{"key":"10.1016\/0167-6423(88)90026-3_BIB30","unstructured":"C.L. Talcott, Program and proving with function and control abstractions, Unpublished manuscript."},{"key":"10.1016\/0167-6423(88)90026-3_BIB31","series-title":"Ph.D. Thesis","article-title":"Decidable pairing functions","author":"Tenney","year":"1972"},{"key":"10.1016\/0167-6423(88)90026-3_BIB32","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00289067","article-title":"The correctness of the Schorr-Waite list marking algorithm","volume":"11","author":"Topor","year":"1979","journal-title":"Acta Inform."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642388900263?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0167642388900263?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T12:29:05Z","timestamp":1555072145000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0167642388900263"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,4]]},"references-count":32,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1988,4]]}},"alternative-id":["0167642388900263"],"URL":"https:\/\/doi.org\/10.1016\/0167-6423(88)90026-3","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[1988,4]]}}}