{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:59:26Z","timestamp":1748350766915,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167808"},{"type":"electronic","value":"9783540398615"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16780-3_99","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:59:19Z","timestamp":1330196359000},"page":"306-315","source":"Crossref","is-referenced-by-count":10,"title":["An interactive verification system based on dynamic logic"],"prefix":"10.1007","author":[{"given":"R.","family":"H\u00e4hnle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Heisel","sequence":"additional","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,5,31]]},"reference":[{"key":"25_CR1","unstructured":"Dijkstra, E.W. A Discipline of Programming. Prentice-Hall (1976)"},{"key":"25_CR2","unstructured":"Goldblatt, R. Axiomatising the Logic of Computer Programming. Springer-LNCS 130 (1982)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Gordon, M. & Milner, R. & Wadsworth, C. Edinburgh-LCF. Springer-LNCS 78 (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"25_CR4","first-page":"287","volume":"118","author":"P. Hajek","year":"1981","unstructured":"Hajek, P. Making dynamic logic first order. Proc. Math. Foundations of Computer Science, Springer-LNCS 118 (1981), 287\u2013295","journal-title":"Proc. Math. Foundations of Computer Science"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Harel, D. First Order Dynamic Logic. Springer-LNCS 68 (1979)","DOI":"10.1007\/3-540-09237-4"},{"key":"25_CR6","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":"Handbook of Philosophical Logic"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R. & Heisel, M. & Reif, W. & Stephan, W. The Karlsruhe Interactive Verifier \u2014 A Verification System based on Dynamic Logic. Interner Bericht 1\/86, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (1986)","DOI":"10.1007\/3-540-16780-3_99"},{"key":"25_CR8","first-page":"576","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R. An axiomatic basis for computer programming. C.A.C.M. 12 (1969), 576\u2013580","journal-title":"C.A.C.M."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Pratt, V.R. Semantical considerations on Floyd-Hoare logic. Proc. 17th Ann. I.E.E.E. Symp. on Foundations of Computer Science, 109\u2013121","DOI":"10.1109\/SFCS.1976.27"},{"key":"25_CR10","unstructured":"Prawitz, D. Natural Deduction. Stockholm Studies in Philosophy 3, Almquist & Wicksell, Stockholm (1965)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Richter, M.M. Logikkalk\u00fcle. Teubner (1978)","DOI":"10.1007\/978-3-322-91208-4"},{"key":"25_CR12","unstructured":"Reif, W. & Stephan, W. Vollst\u00e4ndigkeit einer modifizierten Goldblatt-Logik und Approximation der Omegaregel durch Induktion. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (1984)"},{"key":"25_CR13","first-page":"445","volume":"170","author":"D.A. Schmidt","year":"1984","unstructured":"Schmidt, D.A. A programming notation for tactical reasoning. Proc. 7th Int. Conf. on Automated Deduction, R.E. Shostak (ed.), Springer-LNCS 170 (1984), 445\u2013460","journal-title":"Proc. 7th Int. Conf. on Automated Deduction"},{"key":"25_CR14","unstructured":"Stephan, W. A Logic for Recursive Programs. Interner Bericht 5\/85, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (1985)"}],"container-title":["Lecture Notes in Computer Science","8th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16780-3_99.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:30:50Z","timestamp":1742589050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_99"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_99","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}