{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:34:37Z","timestamp":1725737677316},"publisher-location":"Berlin, Heidelberg","reference-count":48,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540189039"},{"type":"electronic","value":"9783642734052"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/978-3-642-73405-2_4","type":"book-chapter","created":{"date-parts":[[2013,6,25]],"date-time":"2013-06-25T19:43:51Z","timestamp":1372189431000},"page":"134-182","source":"Crossref","is-referenced-by-count":0,"title":["Programmverifikation"],"prefix":"10.1007","author":[{"given":"Volker","family":"Penner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","first-page":"431","volume-title":"Ten years of Hoare\u2019s logic: a survey-part I","author":"KR Apt","year":"1981","unstructured":": Apt,K.R.: Ten years of Hoare\u2019s logic: a survey-part I. ACM Toplas 3, 431\u2013483 (1981)"},{"key":"4_CR2","volume-title":"Formal Methods of Program Verification and Specification","author":"HK Berg","year":"1982","unstructured":": H.K. Berg, W.E. Boebert, W.R. Franta, T.G. Moher: Formal Methods of Program Verification and Specification, Prentice Hall, 1982"},{"key":"4_CR3","volume-title":"A Computational Logic, ACM Monograph Series","author":"BS Boyer","year":"1979","unstructured":": B.S. Boyer, J.S. Moore: A Computational Logic, ACM Monograph Series, Academic Press, 1979"},{"key":"4_CR4","volume-title":"A Prototype Theorem Prover for a higher order Functional Language","author":"BS Boyer","year":"1984","unstructured":": B.S. Boyer, M. Kaufmann: A Prototype Theorem Prover for a higher order Functional Language, Burroughs Corp., Austin, Tex., Dec. 1984"},{"issue":"1","key":"4_CR5","first-page":"17","volume":"Vol. 1","author":"BS Boyer","year":"1985","unstructured":"B.S. Boyer, J.S. Moore: Program Verification, J. of Automated Reasoning, Vol. 1, No 1, 1985, pp 17\u201323","journal-title":"J. of Automated Reasoning"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":": W.W. Bledsoe, P. Bruell: A man-machine theoremproving system, Advance Papers of Third Int. Joint Conf. on.Art. Intelligence, 5\u20131, 1974","DOI":"10.1016\/0004-3702(74)90009-5"},{"key":"4_CR7","first-page":"365","volume-title":"The logic of aliasing","author":"R Cartwright","year":"1981","unstructured":": R. Cartwright, D. Oppen: The logic of aliasing, Acta Informatica 15, 1981, 365\u2013384"},{"key":"4_CR8","first-page":"279","volume-title":"Verifying Security","author":"MH Cheheyl","year":"1981","unstructured":": M.H. Cheheyl, M.G. Gasser, G.A. Huff, J.K. Millen: Verifying Security, in ACM Comp. Surveys, Vol. 13, No 3, Sept. 1981, pp 279\u2013340"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":": Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare-like axioms, J. Ass. Compo Mach. 26, pp 129\u2013147","DOI":"10.1145\/322108.322121"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":": E.M. clarke, S.M. German, J.Y. Halpern: Effective Axiomatization of Hoare logiCS, J. Ass. Compo Mach., 30, 612\u2013636","DOI":"10.1145\/2402.322394"},{"key":"4_CR11","first-page":"267","volume-title":"The equivalence of two semantic definitions: a case study-in LCF","author":"AJ Cohn","year":"1983","unstructured":": A.J. Cohn: The equivalence of two semantic definitions: a case study-in LCF, SIAM J. Compo 12, 267\u2013285, 1983"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":": S.A. Cook: Soundness and completeness of an axiom system for program verification, SIAM J. Compo 7, 70\u201390","DOI":"10.1137\/0207005"},{"key":"4_CR13","volume-title":"A sound and relatively complete Hoarelogic for a language with higher type procedures","author":"W Damm","year":"1982","unstructured":": W. Damm, B. Josko: A sound and relatively complete Hoarelogic for a language with higher type procedures, Tech. Rep. Bericht, no. 77, RWTH Aachen, 1982"},{"key":"4_CR14","volume-title":"Mathematical Theory of Program Correctness","author":"J Bakker de","year":"1980","unstructured":": J. de Bakker: Mathematical Theory of Program Correctness, Prentice Hall, 1980"},{"key":"4_CR15","volume-title":"Overview of the \u2018Ina Jo\u2019 specification language","author":"PR Eggert","year":"1980","unstructured":": P.R. Eggert: Overview of the \u2018Ina Jo\u2019 specification language, Techn. Rep. SP 4082, System Development Corp., Santa Monica, Calif., Oct 1980"},{"key":"4_CR16","volume-title":"Formale Analyse und Verifikation von Pro grammen","author":"A Endres","year":"1976","unstructured":": A. Endres: Formale Analyse und Verifikation von Pro grammen, Dissertation Stuttgart 1976"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer ScienceAssigning meanings to programs","author":"RW Floyd","year":"1967","unstructured":": R.W. Floyd: Assigning meanings to programs, in: Mathematical Aspects of Computer Science, J.T. Schwartz (ed.), AMS, 1967, pp 19\u201332"},{"key":"4_CR18","volume-title":"Nucleus - a language of provable programsProgram Test Methods","author":"DI Good","year":"1974","unstructured":": D.I. Good, L.C. Ragland: Nucleus - a language of provable programs, in W. Hetzel (ed.), Program Test Methods, Prentice Hall, 1974"},{"key":"4_CR19","unstructured":": D.I. Good, R.M. Cohen, L.W. Hunter: A report on the development of Gypsy, Techn. Rep. ICSCA-CMP-13, Univ. Tex. Austin,78"},{"key":"4_CR20","volume-title":"Report on the language Gypsy","author":"DI Good","year":"1978","unstructured":": D.I. Good, R.M. Cohen, C.G. Hoch, L.W. Hunter, D.F. Hare: Report on the language Gypsy, Version 2.0, Techn. Rep. ICSCACMP- 10, Univ. Tex. Austin, Sept. 1978"},{"key":"4_CR21","unstructured":": J.A. Goguen, J.W. Thatcher, E.G. Wagner: Abstract data types as initial algebras and the correctness of data representation, in: Current Trends in Programming Methodology, Yeh (ed.), Vol. 4, pp 80\u2013149,1978"},{"key":"4_CR22","first-page":"27","volume-title":"The algebraic specification of abstract data types","author":"JV Guttag","year":"1978","unstructured":": J.V. Guttag, J.J. Hornig: The algebraic specification of abstract data types, Acta Informatica 10, pp 27\u201352,1978"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":": J.Y. Halpern, A.R. Meyer, B.A. Trakhtenbrot: From denotational to operational and axiomatic semantics, in: Lect. Notes Compo Sci., no. 164, Springer 1983, pp 474\u2013500","DOI":"10.1007\/3-540-12896-4_382"},{"key":"4_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09237-4","volume-title":"First-order dynamic logic, Lect. Notes Comp. Sci","author":"D Harel","year":"1979","unstructured":": D. Harel: First-order dynamic logic, Lect. Notes Compo Sci., no. 68, Springer, 1979"},{"key":"4_CR25","first-page":"576","volume-title":"An axiomatic basis of computer programming","author":"CAR Hoare","year":"1969","unstructured":": C.A.R. Hoare: An axiomatic basis of computer programming, Comm. ACM, 12, pp. 576\u2013583,1969"},{"key":"4_CR26","first-page":"321","volume-title":"Proof of a structured program: \u2018The sieve of Eratosthenes\u2019","author":"CAR Hoare","year":"1972","unstructured":": C.A.R. Hoare: Proof of a structured program: \u2018The sieve of Eratosthenes\u2019, Compo J., Vol. 15, pp. 321\u2013325, 1972"},{"key":"4_CR27","first-page":"271","volume-title":"Proof of correctness of data representations","author":"CAR Hoare","year":"1972","unstructured":": C.A.R. Hoare: Proof of correctness of data representations, Acta Informatica, vol. 1, pp. 271\u2013281, 1972"},{"key":"4_CR28","first-page":"11","volume-title":"The relation between logic programming and logic specification, in: Mathematical LogiC and Programming Languages","author":"R Kowalski","year":"1985","unstructured":": R. Kowalski: The relation between logic programming and logic specification, in: Mathematical LogiC and Programming Languages, Prentice Hall, pp. 11\u201324, 1985"},{"key":"4_CR29","volume-title":"Report on the Programming Languaqe Euclid","author":"BW Lampson","year":"1977","unstructured":": B.W. Lampson, J.J. Hornig, R.L. London, J.G. Mitchell, G.J. Popek: Report on the Programming Languaqe Euclid, Siqplan Notices, 12(2), Febr. 1977"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Langmaack,Olderog 80: H. Langmaack,E.R. Olderog: Present-day Hoarelike systems for programming languages with procedures power, limits and most likely extensions, in: Automata, Languages and Programming, Lect. Notes Compo Sci. 83, 363\u2013373, 1980","DOI":"10.1007\/3-540-10003-2_84"},{"key":"4_CR31","volume-title":"The HOM Handbook","author":"KN Levitt","year":"1979","unstructured":": K.N. Levitt, L. Robinson, B.A. Silverberg: The HOM Handbook, Vols. 1\u20133, Compo Sci. Lab., SRI International, Menlo Parc, Calif., June 1979"},{"key":"4_CR32","first-page":"1","volume-title":"A necessary and sufficient condition for the existence of Hoare logics","author":"RJ Lipton","year":"1977","unstructured":": R.J. Lipton: A necessary and sufficient condition for the existence of Hoare logics, Proc. 18th IEEE Symp. Found. Compo ScL, pp. 1\u20136, 1977"},{"key":"4_CR33","volume-title":"Specification techniques for data abstractions","author":"BH Liskov","year":"1975","unstructured":": B.H. Liskov, S.N. Zilles: Specification techniques for data abstractions, IEEE Trans. Softw. Eng., Vol. SE-1, No.1., March 1975"},{"key":"4_CR34","volume-title":"The Foundation of Program Verification","author":"J Loeckx","year":"1984","unstructured":": J. Loeckx, K. Sieber: The Foundation of Program Verification, Wiley, 1984"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":": P. Lucas, K. Walk: On the formal description of PL\/1, in Annual Review in Automatic Progr. 6, Pergamon,105\u2013182, 1971","DOI":"10.1016\/0066-4138(69)90005-6"},{"key":"4_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/942578.807067","volume":"7","author":"R Milner","year":"1972","unstructured":": R. Milner: Logic for computable functions: description of a machine implementation, Siqplan Notices, 7, 1\u20136, 1972","journal-title":"Siqplan Notices"},{"key":"4_CR37","volume-title":"Towards the Generation of efficient Code from verified Programs","author":"J McHugh","year":"1984","unstructured":": J. McHugh: Towards the Generation of efficient Code from verified Programs, Techn. Rep. 40, ICSCA Univ. Tex.,1984"},{"key":"4_CR38","first-page":"310","volume-title":"Proof of algorithms by general snapshots","author":"P Naur","year":"1966","unstructured":": P. Naur: Proof of algorithms by general snapshots, BIT 6, pp. 310\u2013316, 1966"},{"key":"4_CR39","unstructured":"N\u00f6kel,Rehbold 85: K. N\u00f6kel: Implementierung einer Reduktionsmaschine und Steuerung und Organisation eines Beweissystems fur eine Logik, Diplomarbeit, RWTH Aachen, 1985. Ebenso R. Rehbold: Implementierung eines Abstraktionsalgorithmus und Beweisalgorithmen fur eine Logik"},{"key":"4_CR40","first-page":"161","volume-title":"Sound and complete Hoare-like calculi based on copy rules","author":"ER Olderog","year":"1981","unstructured":": E.R. Olderog: Sound and complete Hoare-like calculi based on copy rules, Acta Informatica 16, pp. 161\u2013197, 1981"},{"key":"4_CR41","volume-title":"A Technique for Software Module Specification with Examples","author":"DL Parnas","year":"1972","unstructured":": D.L. Parnas: A Technique for Software Module Specification with Examples, Comm. ACM, Vol. 15, May 1972"},{"key":"4_CR42","volume-title":"On the Criteria to be used in decomposing Systems into Modules","author":"DL Parnas","year":"1972","unstructured":": D.L. Parnas: On the Criteria to be used in decomposing Systems into Modules, Comm. ACM, Vol 15, Dec. 1972"},{"key":"4_CR43","volume-title":"SPECIAL Reference Manual","author":"O Roubine","year":"1977","unstructured":": O. Roubine, L. Robinson: SPECIAL Reference Manual, Techn. Rep. CSG-45, SRI, Menlo Parc, Calif., Jan. 1977"},{"key":"4_CR44","volume-title":"Towards a Mathematical Semantics for Computer Languages","author":"DS Scott","year":"1971","unstructured":": D.S. Scott, C. Strachey: Towards a Mathematical Semantics for Computer Languages, Proc. Symp. Compo and Automata, Polytechn. Inst. Brooklyn Press, New York, 1971"},{"key":"4_CR45","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"JE Stoy","year":"1977","unstructured":": J.E. Stoy: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, The MIT Press,1977"},{"key":"4_CR46","volume-title":"EMACS:The Extensible, Customizable Display Editor","author":"RM Stallman","year":"1981","unstructured":": R.M. Stallman: EMACS:The Extensible, Customizable Display Editor, MIT Art. Intell. Lab., Memo 519a, 1981"},{"key":"4_CR47","volume-title":"A necessary and sufficient condition in order that a Herbrand interpretation is expressive relative to recursive programs","author":"P Urzyczyn","year":"1983","unstructured":": P. Urzyczyn: A necessary and sufficient condition in order that a Herbrand interpretation is expressive relative to recursive programs, Inst. Mathern., Univ. Warsaw, 1983"},{"key":"4_CR48","first-page":"221","volume-title":"Program development by stepwise refinement","author":"N Wirth","year":"1971","unstructured":": N. Wirth: Program development by stepwise refinement, Comm. ACM 14, pp. 221\u2013227, April 1971"}],"container-title":["Informatik-Fachberichte","K\u00fcnstliche Intelligenz"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-73405-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T15:46:23Z","timestamp":1557848783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-73405-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540189039","9783642734052"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-73405-2_4","relation":{},"ISSN":["0343-3005"],"issn-type":[{"type":"print","value":"0343-3005"}],"subject":[],"published":{"date-parts":[[1988]]}}}