{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:15Z","timestamp":1751660535472},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1977,3,1]],"date-time":"1977-03-01T00:00:00Z","timestamp":226022400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1977,3,1]],"date-time":"1977-03-01T00:00:00Z","timestamp":226022400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1977,3]]},"DOI":"10.1007\/bf00276182","type":"journal-article","created":{"date-parts":[[2023,7,4]],"date-time":"2023-07-04T16:18:03Z","timestamp":1688487483000},"page":"21-36","source":"Crossref","is-referenced-by-count":9,"title":["Proof of termination within a weak logic of programs"],"prefix":"10.1007","volume":"8","author":[{"given":"David C.","family":"Luckham","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Norihisa","family":"Suzuki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF00276182_CR1","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/BF00571463","volume":"2","author":"M. Clint","year":"1973","unstructured":"Clint, M.: Program proving: Coroutine. Acta Informatica 2, 50\u201363 (1973)","journal-title":"Acta Informatica"},{"key":"BF00276182_CR2","volume-title":"Ph. D. thesis","author":"L.P. Deutsch","year":"1973","unstructured":"Deutsch, L.P.: An interactive program verifier. University of California, Berkeley, Ph. D. thesis (1973)"},{"key":"BF00276182_CR3","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"Vol. 18","author":"E. Dijkstra","year":"1975","unstructured":"Dijkstra, E.: Guarded Commands, Nondeterminacy, and formal derivation, Comm. ACM, Vol. 18, pp. 453\u2013457 (1975)","journal-title":"Comm. ACM"},{"key":"BF00276182_CR4","unstructured":"Farmwald, M.: Private communications. A I Laboratory, Stanford University (1975)"},{"key":"BF00276182_CR5","first-page":"19","volume-title":"Proc. Sbymp. Appl. Math., Vol.19","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Acssigning meanings to programs. Proc. Sbymp. Appl. Math., Vol.19, pp. 19\u201332. Providence (R. I.): Amer. Math. Soc. 1967"},{"key":"BF00276182_CR6","doi-asserted-by":"crossref","unstructured":"von Henke, F.W., Luckham, D.C.: A methodology for verifying programs. Proc. of Int. Conf. of Reliable Software, IEEE, pp. 156\u2013164 (1975)","DOI":"10.1145\/390016.808435"},{"key":"BF00276182_CR7","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"Vol. 12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM, Vol. 12, pp. 576\u2013580 (1969)","journal-title":"Comm. ACM"},{"key":"BF00276182_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symposium on semantics of algorithmic languages","author":"C.A.R. Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Symposium on semantics of algorithmic languages. Lecture notes in computer science. (E. Engeler, ed.), Vol. 188, pp. 102\u2013116. Berlin-Heidelberg-New York: Springer 1971"},{"key":"BF00276182_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\u2013355 (1973)","journal-title":"Acta Informatica"},{"key":"BF00276182_CR10","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S. Igarashi","year":"1975","unstructured":"Igarashi, S., London, R.L., Luckham, D.C.: Automatic program verification. Logical basis and its implementation. Acta Informatica 4, 145\u2013182 (1975)","journal-title":"Acta Informatica"},{"key":"BF00276182_CR11","unstructured":"King, J.C.: A program verifier. Carnegie-Mellon University, Ph. D. thesis (1969)"},{"key":"BF00276182_CR12","first-page":"17","volume-title":"The art of computer programming, Vol. 1","author":"D.E. Knuth","year":"1973","unstructured":"Knuth, D.E.: Fundamental algorithms. In: The art of computer programming, Vol. 1, pp. 17\u201319. Reading (Mass.): Addison-Wesley 1973"},{"key":"BF00276182_CR13","doi-asserted-by":"crossref","unstructured":"Luckham, D.C., Suzuki, N.: Automatic program verification. IV. Proof of termination within a weak logic of programs. Stanford Artificial Intelligence Project, Stanford University, AIM-269 (1975)","DOI":"10.21236\/ADA019569"},{"key":"BF00276182_CR14","doi-asserted-by":"crossref","unstructured":"Suzuki, N.: Verifying programs by algebraic and logical reduction. Proc. of Int. Conf. on Reliable Software, IEEE, pp. 473\u2013481 (1975)","DOI":"10.1145\/390016.808471"},{"key":"BF00276182_CR15","unstructured":"Suzuki, N.: Automatic verification of program with complex data structure. Stanford University, Ph. D. Thesis (1976)"},{"key":"BF00276182_CR16","unstructured":"Waldinger, R.J., Levitt, K.N.: Reasoning about programs. Stanford Research Institute, SRI Project 2245, Technical Note 86 (1974)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00276182.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/BF00276182\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00276182.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,4]],"date-time":"2023-07-04T16:18:12Z","timestamp":1688487492000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BF00276182"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1977,3]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1977,3]]}},"alternative-id":["BF00276182"],"URL":"https:\/\/doi.org\/10.1007\/bf00276182","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1977,3]]}}}