{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:32:01Z","timestamp":1725467521601},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055137","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"189-206","source":"Crossref","is-referenced-by-count":2,"title":["Mechanical verification of total correctness through diversion verification conditions"],"prefix":"10.1007","author":[{"given":"Peter V.","family":"Homeier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David F.","family":"Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"issue":"2","key":"12_CR1","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90037-I","volume":"84","author":"P. America","year":"1990","unstructured":"P. America and F. de Boer. Proving Total Correctness of Recursive Procedures. Information and Computation, 84(2):129\u2013162, 1990.","journal-title":"Information and Computation"},{"issue":"4","key":"12_CR2","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. R. Apt","year":"1981","unstructured":"K. R. Apt. Ten Years of Hoare logic: A Survey \u2014 Part 1. ACM TOPLAS, 3(4):431\u2013483, 1981.","journal-title":"ACM TOPLAS"},{"key":"12_CR3","volume-title":"Introduction to HOL, A Theorem Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"M. Gordon and T. Melham. Introduction to HOL, A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, 1993."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. Procedures and Parameters: an axiomatic approach. In: Proceedings of Symposium on Semantics of Algorithmic Languages, ed. E. Engeler, volume 188 of Lecture Notes in Mathematics, pages 102\u2013116, 1971.","DOI":"10.1007\/BFb0059696"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"P. Homeier. Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures. Ph.D. Dissertation, UCLA Computer Science Department, 1995.","DOI":"10.1007\/3-540-58450-1_48"},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1093\/comjnl\/38.2.131","volume":"38","author":"P. Homeier","year":"1995","unstructured":"P. Homeier and D. Martin. A Mechanically Verified Verification Condition Generator. The Computer Journal, 38(2):131\u2013141, 1995.","journal-title":"The Computer Journal"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"P. Homeier and D. Martin. Mechanical Verification of Mutually Recursive Procedures. In M. A. McRobbie and J. K. Slaney (eds.), Proceedings of the 13th International Conference on Automated Deduction (CADE-13), volume 1104 of Lecture Notes in Artificial Intelligence, pages 201\u2013215, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_81"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/BF00288746","volume":"4","author":"S. Igarashi","year":"1975","unstructured":"S. Igarashi, R. L. London, and C. Luckham. Automatic program verification: A logical basis and its implementation. Acta Informatica, 4:145\u2013182, 1975.","journal-title":"Acta Informatica"},{"key":"12_CR9","first-page":"350","volume-title":"A Package for Inductive Relation Definitions in HOL","author":"T. Melham","year":"1992","unstructured":"T. Melham. A Package for Inductive Relation Definitions in HOL. In M. Archer, J. Joyce, K. Levitt, and Windley (eds.), Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991. IEEE Computer Society Press, pages 350\u2013357, 1992."},{"issue":"6","key":"12_CR10","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1093\/comjnl\/29.6.531","volume":"29","author":"P. Pandya","year":"1986","unstructured":"P. Pandya and M. Joseph. A Structure-directed Total Correctness Proof Rule for Recursive Procedure Calls. The Computer Journal, 29(6):531\u2013537, 1986.","journal-title":"The Computer Journal"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"S. Sokolowski. Total Correctness for Procedures, In J. Gruska (ed), Proceedings, 6th Symposium on the Mathematical Foundations of Computer Science, volume 53 of Lecture Notes in Computer Science, pages 475\u2013483, Springer-Verlag, 1977.","DOI":"10.1007\/3-540-08353-7_170"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055137","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:34:33Z","timestamp":1555734873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055137"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0055137","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}