{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:05Z","timestamp":1762458965219},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540512370"},{"type":"electronic","value":"9783540461807"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51237-3_12","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:48:21Z","timestamp":1330202901000},"page":"134-145","source":"Crossref","is-referenced-by-count":16,"title":["A dynamic logic for program verification"],"prefix":"10.1007","author":[{"given":"M.","family":"Heisel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W.","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"W.","family":"Stephan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Andreka, H., Nemeti, I., Sain, I. A Complete Logic for Reasoning about Programs via Nonstandard Model Theory, Part I, II, Theoretical Computer Science 17, pp. 139\u2013212, 259\u2013278","DOI":"10.1016\/0304-3975(82)90025-1"},{"key":"12_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(84)90065-3","volume":"30","author":"J. A. Bergstra","year":"1984","unstructured":"Bergstra, J. A., Klop, J. W. Proving Program Inclusion Using HOARE's Logic, Theoretical Computer Science 30 (1984), pp. 1\u201348","journal-title":"Theoretical Computer Science"},{"key":"12_CR3","unstructured":"de Bruijn, N.G. A Survey of the Project AUTOMATH. Essays in Combinatory Logic, Lambda Calculus, and Formalism, J.P. Seldin and J.R. Hindley (eds.) Academic Press (1980), pp 589\u2013606"},{"key":"12_CR4","unstructured":"Burstall, R.M. Program Proving as Hand Simulation with a little Induction. Information Processing 74, North-Holland Publishing Company (1974)"},{"issue":"3","key":"12_CR5","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00244273","volume":"1","author":"R. Constable","year":"1985","unstructured":"Constable, R.\/Knoblock, T.\/Bates, J. Writing Programs That Construct Proofs. Journal of Automated Reasoning, Vol.1, No.3, pp 285\u2013326 (1985)","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR6","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/BF00264295","volume":"20","author":"W. Damm","year":"1983","unstructured":"Damm, W.\/Josko, B. A sound and relatively* complete Hoare-logic for a language with higher type procedures, Acta Informatica 20 (1983), pp. 59\u2013101","journal-title":"Acta Informatica"},{"key":"12_CR7","unstructured":"Goldblatt, R. Axiomatising the Logic of Computer Programming. Springer LNCS 130 (1982)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Gries, D. The Science of Programming, Springer-Verlag (1981)","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Harel, D. First Order Dynamic Logic. Springer LNCS 68 (1979)","DOI":"10.1007\/3-540-09237-4"},{"key":"12_CR10","first-page":"496","volume":"2","author":"D. Harel","year":"1984","unstructured":"Harel, D. Dynamic Logic. Handbook of Philosophical Logic, D. Gabbay and F. Guenther (eds.), Reidel (1984), Vol. 2, 496\u2013604","journal-title":"Reidel"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Hailpern, B. Keeping a Foot on the Ground, Logics of Programs, Proceedings 81, LNCS 131, pp. 122\u2013123","DOI":"10.1007\/BFb0025778"},{"key":"12_CR12","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 (1969), pp. 576\u2013580, 583","journal-title":"Comm. ACM"},{"key":"12_CR13","unstructured":"Heisel,M.\/Reif, W.\/Stephan, W. A Functional Language to Construct Proofs. Interner Bericht 1\/86, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (1986)"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Heisel,M.\/Reif, W.\/Stephan, W. Program Verification by Symbolic Execution and Induction. Proc. 11-th German Workshop on Artificial Intelligence, K. Morik (ed), Informatik Fachberichte 152, Springer-Verlag (1987)","DOI":"10.1007\/978-3-642-73005-4"},{"key":"12_CR15","first-page":"131","volume":"310","author":"M. Heisel","year":"1988","unstructured":"Heisel, M.\/Reif, W.\/Stephan, W. Implementing Verification Strategies in the KIV System. Proc. 9-th International Conference on Automated Deduction, E. Lusk\/R. Overbeek (eds), Springer LNCS 310 (1988), pp. 131\u2013140","journal-title":"Springer LNCS"},{"key":"12_CR16","unstructured":"Heisel,M.\/Reif, W.\/Stephan, W. Reasoning about imperative programs with dynamic logic. Submitted for publication."},{"key":"12_CR17","unstructured":"Manna, Z. Mathematical Theory of Computation. McGraw Hill (1974)"},{"key":"12_CR18","unstructured":"Manna, Z. Verification of Sequential Programs: Temporal Axiomatization. Theoretical Foundations of Programming Methodology, Nato Advanced Study Institutes Series C91, D. Reidel, (1981)"},{"key":"12_CR19","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0304-3975(84)90066-5","volume":"30","author":"E. R. Olderog","year":"1984","unstructured":"Olderog, E. R. Correctness of Programs with Pascal-like Procedures without Global Variables, Theoretical Computer Science 30 (1984), pp. 49\u201390","journal-title":"Theoretical Computer Science"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Pasztor, A. Non-standard Algorithmic and Dynamic Logic, Journal of Symbolic Computation (86) 2, pp. 59\u201381.","DOI":"10.1016\/S0747-7171(86)80013-X"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Pnueli, A. The Temporal Logic of Programs, The 18th Annual Symposium on Foundations of Computer Science (Providence, Rhode Island), pp. 46\u201357, IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"12_CR22","unstructured":"Salwicki, A. Formalized Algorithmic Languages. Bull. Acad. Pol. Sci., Ser. Sci. Math. Astr. Phys. Vol. 18, No. 5 (1970)"},{"key":"12_CR23","unstructured":"Stephan, W. A Logic for Recursive Programs. Interner Bericht 5\/85, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (1985)"},{"key":"12_CR24","unstructured":"Stephan, W. Axiomatising Recursive Procedures in Dynamic Logic. Forthcoming (1989)"}],"container-title":["Lecture Notes in Computer Science","Logic at Botik '89"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51237-3_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:20:19Z","timestamp":1605648019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51237-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540512370","9783540461807"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-51237-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}