{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:06Z","timestamp":1749124086191},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540528852"},{"type":"electronic","value":"9783540471714"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52885-7_83","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:47:42Z","timestamp":1330206462000},"page":"117-131","source":"Crossref","is-referenced-by-count":23,"title":["Tactical theorem proving in program verification"],"prefix":"10.1007","author":[{"given":"M.","family":"Heisel","sequence":"first","affiliation":[]},{"given":"W.","family":"Reif","sequence":"additional","affiliation":[]},{"given":"W.","family":"Stephan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"9_CR1","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":"9_CR2","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S.\/ Moore, J.S. A Computational Logic. Academic Press, New York 1979"},{"key":"9_CR3","unstructured":"Burstall, R.M. Program Proving as Hand Simulation with a little Induction. Information Processing 74, North-Holland Publishing Company (1974)"},{"key":"9_CR4","first-page":"57","volume-title":"Automatic Guidance of Program Synthesis Proofs","author":"A. Bundy","year":"1989","unstructured":"Bundy, A. Automatic Guidance of Program Synthesis Proofs. Proc. Workshop on Automating Software Design, IJCAI 89. Kestrel Institute, Palo Alto (1989), pp. 57\u201359"},{"key":"9_CR5","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. Constable","year":"1986","unstructured":"Constable, R. et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)"},{"key":"9_CR6","unstructured":"E.W. Dijkstra. Lecture held on 8\/4\/1988, International Summer School \"Constructive Methods in Computing Science\", Marktoberdorf 1988."},{"key":"9_CR7","first-page":"61","volume":"310","author":"A. Felty","year":"1988","unstructured":"Felty, A.\/Miller, D. Specifying Theorem Provers in a Higher-Oder Logic Programming Language. Proc. 9-th International Conference on Automated Deduction, E. Lusk, R. Overbeek (eds), Springer LNCS 310 (1988), pp. 61\u201380","journal-title":"Springer LNCS"},{"key":"9_CR8","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":"9_CR9","unstructured":"Goldblatt, R. Axiomatising the Logic of Computer Programming. Springer LNCS 130 (1982)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Gries, D. The Science of Programming, Springer-Verlag (1981)","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Harel, D. First Order Dynamic Logic. Springer LNCS 68 (1979)","DOI":"10.1007\/3-540-09237-4"},{"key":"9_CR12","unstructured":"H\u00e4hnle, R. Programmverifikation durch symbolische Ausf\u00fchrung und Induktion. Diplomarbeit, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (1987)"},{"key":"9_CR13","unstructured":"Heisel, M. A Formalization and Implementation of Gries's Program Development Method within the KIV Environment. Int. Bericht 3\/89, Fak. f\u00fcr Informatik, Univ. Karlsruhe"},{"key":"9_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":"9_CR15","first-page":"134","volume":"363","author":"M. Heisel","year":"1989","unstructured":"Heisel, M.\/Reif, W.\/Stephan, W. A Dynamic Logic for Program Verification. Proc. Logic at Botik 89, A. Meyer, M. Taitslin (eds), Springer LNCS 363 (1989), pp. 134\u2013145","journal-title":"Springer LNCS"},{"key":"9_CR16","first-page":"460","volume":"170","author":"K. Mulmuly","year":"1984","unstructured":"Mulmuly, K. Mechanization of existence proofs of recursive functions. Proc. 7-th International Conference on Automated Deduction, Springer LNCS 170 (1984), pp. 460\u2013475","journal-title":"Springer LNCS"},{"key":"9_CR17","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"Oppacher, F.\/Suen, E. HARP: A Tableau-Based Theorem Prover. Journal of Automated Reasoning, Vol. 4 (1988), pp. 69\u2013100.","journal-title":"Journal of Automated Reasoning"},{"key":"9_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511526602","volume-title":"Logic and computation","author":"L. Paulson","year":"1987","unstructured":"Paulson, L. Logic and computation. Cambridge University Press, Cambridge (1987)"},{"key":"9_CR19","unstructured":"Reif, W. Vollst\u00e4ndigkeit einer modifizierten Goldblatt-Logik und Approximation der Omegaregel durch Induktion. Diplomarbeit, Fak. f\u00fcr Informatik, Univ. Karlsruhe (1984)"},{"key":"9_CR20","unstructured":"Stephan, W. A Logic for Recursive Programs. Interner Bericht 5\/85, Fak. f\u00fcr Informatik, Universit\u00e4t Karlsruhe (1985)"}],"container-title":["Lecture Notes in Computer Science","10th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52885-7_83.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:36Z","timestamp":1605648336000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52885-7_83"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540528852","9783540471714"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-52885-7_83","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}