{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:46:06Z","timestamp":1773654366930,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540108436","type":"print"},{"value":"9783540387459","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1981]]},"DOI":"10.1007\/3-540-10843-2_30","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:28:40Z","timestamp":1330190920000},"page":"363-377","source":"Crossref","is-referenced-by-count":13,"title":["Automatic construction of verification condition generators from hoare logics"],"prefix":"10.1007","author":[{"given":"Mark","family":"Moriconi","sequence":"first","affiliation":[]},{"given":"Richard L.","family":"Schwartz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,25]]},"reference":[{"issue":"1","key":"30_CR1","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E. M. Clarke Jr.","year":"1979","unstructured":"E.M. Clarke, Jr. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Journal of the ACM, 26,1, pp. 129\u2013147, January 1979.","journal-title":"Journal of the ACM"},{"issue":"1","key":"30_CR2","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S. A. Cook","year":"1978","unstructured":"S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing, Vol. 7, No. 1, pp. 70\u201390, February 1978.","journal-title":"SIAM Journal of Computing"},{"key":"30_CR3","volume-title":"A discipline of programming","author":"E. W. Dijkstra","year":"1976","unstructured":"E.W. Dijkstra. A discipline of programming. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1976."},{"issue":"10","key":"30_CR4","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, vol. 12, no. 10, pp. 576\u2013580, October 1969.","journal-title":"Communications of the ACM"},{"issue":"4","key":"30_CR5","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C. A. R. R. Hoare","year":"1973","unstructured":"C.A.R. Hoare and N. Wirth. An axiomatic definition of the programming language Pascal. Acta Informatica, 2, 4, pp. 335\u2013355, 1973.","journal-title":"Acta Informatica"},{"key":"30_CR6","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S. Igarashi","year":"1975","unstructured":"S. Igarashi, R.L. London, D.C. Luckham. Automatic program verification I: A logical basis and its implementation. Acta Informatica, 4, pp. 145\u2013182, 1975.","journal-title":"Acta Informatica"},{"key":"30_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00260921","volume":"10","author":"R. L. London","year":"1978","unstructured":"R.L. London, J.V. Guttag, J.J. Horning, B.W. Lampson, J.G. Mitchell, and G.J. Popek. Proof rules for the programming language Euclid. Acta Informatica, 10, pp. 1\u201326, 1978.","journal-title":"Acta Informatica"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"A. Meyer and J. Halpern. Axiomatic definitions of programming languages: a theoretical assessment. Seventh Annual ACM Symposium on Principles of Programming Languages, pp. 203\u2013212, January 1980.","DOI":"10.1145\/567446.567466"},{"key":"30_CR9","unstructured":"R. Schwartz. An axiomatic semantic definition of Algol 68. Ph.D. thesis, UCLA Computer Science Department Report UCLA-34-P214-75, August 1978."},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"R. Schwartz. An Axiomatic Treatment of Algol 68 Routines. Proceedings of the International Conference on Automata, Languages and Programming, Springer Verlag Lecture Notes in Computer Science, July 1979.","DOI":"10.1007\/3-540-09510-1_43"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-10843-2_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:03:38Z","timestamp":1605643418000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-10843-2_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1981]]},"ISBN":["9783540108436","9783540387459"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-10843-2_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1981]]}}}