{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T13:18:08Z","timestamp":1762953488187},"reference-count":15,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1975,1,1]],"date-time":"1975-01-01T00:00:00Z","timestamp":157766400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1975]]},"DOI":"10.1007\/bf00288746","type":"journal-article","created":{"date-parts":[[2004,10,4]],"date-time":"2004-10-04T15:29:29Z","timestamp":1096903769000},"page":"145-182","source":"Crossref","is-referenced-by-count":77,"title":["Automatic program verification I: A logical basis and its implementation"],"prefix":"10.1007","volume":"4","author":[{"given":"Shigeru","family":"Igarashi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralph L.","family":"London","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David C.","family":"Luckham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"321","volume-title":"Machine Intelligence 5","author":"J. R. Allen","year":"1970","unstructured":"Allen, J. R., Luckham, D.: An interactive theorem-proving program. In: Meltzer, B., Michie, D. (eds.): Machine Intelligence 5. Edinburgh: Edinburgh University Press 1970, p. 321?336"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/BF00288686","volume":"1","author":"M. Clint","year":"1972","unstructured":"Clint, M., Hoare, C. A. R.: Program proving: Jumps and functions. Acta Informatica 1, 214?224 (1972)","journal-title":"Acta Informatica"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1145\/355588.365103","volume":"7","author":"R. W. Floyd","year":"1964","unstructured":"Floyd, R. W.: Algorithm 245, TREESORT 3. Comm. ACM 7, 701 (1964)","journal-title":"Comm. ACM"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Floyd, R. W.: Assigning meanings to programs. In: Schwartz, J. T. (ed.). Mathematical aspects of computer science. Proc. Symposia in Applied Mathematics 19. Providence (R.I.): Am. Math. Soc. 1967, p. 19?32","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"CR5","first-page":"7","volume-title":"Toward interactive design of correct programs. Proc. IFIP Congress 71","author":"R. W. Floyd","year":"1972","unstructured":"Floyd, R. W.: Toward interactive design of correct programs. Proc. IFIP Congress 71, Amsterdam: North-Holland 1972, p. 7?10"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"Hoare, C. A. R.: An axiomatic basis for computer programming. Comm. ACM 12, 576?580, 583 (1969)","journal-title":"Comm. ACM"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Hoare, C. A. R.: Procedures and parameters: An axiomatic approach. In: Engeler, E. (ed.): Symposium on semantics of algorithmic languages. Lecture Notes in Mathematics 188. Berlin-Heidelberg-New York: Springer 1971, p. 102?116","DOI":"10.1007\/BFb0059696"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/362452.362489","volume":"14","author":"C. A. R. Hoare","year":"1971","unstructured":"Hoare, C. A. R.: Proof of a program: FIND. Comm. ACM 14, 39?45 (1971)","journal-title":"Comm. ACM"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C. A. R. Hoare","year":"1973","unstructured":"Hoare, C. A. R., Wirth, N.: An axiomatic definition of the programming language Pascal. Acta Informatica 2, 335?355 (1973)","journal-title":"Acta Informatica"},{"key":"CR10","volume-title":"Ph.D. Thesis","author":"J. C. King","year":"1969","unstructured":"King, J. C.: A program verifier. Carnegie-Mellon University, Pittsburgh (Pa.). Ph.D. Thesis 1969. See also: Proc. IFIP Congress 71. Amsterdam: North-Holland 1972, p. 234?249"},{"key":"CR11","first-page":"39","volume-title":"The current state of proving programs correct. Proc. of ACM Annual Conference","author":"R. L. London","year":"1972","unstructured":"London, R. L.: The current state of proving programs correct. Proc. of ACM Annual Conference, 1972. New York: ACM, p. 39?46"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Painter, J. A.: Correctness of a compiler for arithmetic expressions. In: Schwartz, J. T. (ed.): Mathematical aspects of computer science. Proc. Symposia in Applied Mathematics 19. Providence(R.I.): Am.Math. Soc.1967, p.33?41","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"CR13","unstructured":"Smith, D. C., Enea, H. J.: MLISP2. Stanford University Artificial Intelligence Memo AIM-195, April 1973"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF00264291","volume":"1","author":"N. Wirth","year":"1971","unstructured":"Wirth, N.: The programming language Pascal. Acta Informatica 1, 35?63 (1971)","journal-title":"Acta Informatica"},{"key":"CR15","volume-title":"The programming language Pascal (Revised Report). Berichte der Fachgruppe Computer-Wissenschaften Nr. 5","author":"N. Wirth","year":"1972","unstructured":"Wirth, N.: The programming language Pascal (Revised Report). Berichte der Fachgruppe Computer-Wissenschaften Nr. 5, E.T. H., Z\u00fcrich, November 1972"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00288746.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00288746\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00288746","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T21:14:26Z","timestamp":1554758066000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00288746"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1975]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1975]]}},"alternative-id":["BF00288746"],"URL":"https:\/\/doi.org\/10.1007\/bf00288746","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1975]]}}}