{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:54:26Z","timestamp":1725663266778},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540083535"},{"type":"electronic","value":"9783540372851"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1977]]},"DOI":"10.1007\/3-540-08353-7_124","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T16:24:35Z","timestamp":1330187075000},"page":"17-33","source":"Crossref","is-referenced-by-count":8,"title":["A comparative review of some program verification methods"],"prefix":"10.1007","author":[{"given":"Andrzej","family":"Blikle","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,24]]},"reference":[{"key":"2_CR1","unstructured":"de Bakker, J.W. The fixed-point approach in semantics: theory and applications. In: Foundations of Comp. Sci. (J.W.de Bakker, Ed.) pp.3\u201353, 1975. Mathematical Centre Tracts 63, Amsterdam 1975"},{"key":"2_CR2","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0022-0000(75)80056-0","volume":"11","author":"J. W. Bakker de","year":"1975","unstructured":"de Bakker, J.W. and Meertens, L.G.L.T. On the completeness of the inductive assertion method. J. Comp.Syst.Sci., 11 (1975), 323\u2013257","journal-title":"J. Comp.Syst.Sci."},{"key":"2_CR3","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1109\/TSE.1975.6312858","volume":"SE-1","author":"S. K. Basu","year":"1975","unstructured":"Basu, S.K. and Yeh, R.T. Strong verification of programs. IEEE Trans. on Software Eng., SE-1 (1975), 339\u2013345.","journal-title":"IEEE Trans. on Software Eng."},{"key":"2_CR4","unstructured":"Beki\u0107, H. Definable operations in general algebras and the theory of automata and flowcharts. unpublished manuscript, IBM Laboratory, Vienna 1969."},{"key":"2_CR5","first-page":"51","volume":"20","author":"A. Blikle","year":"1971","unstructured":"Blikle, A. Iterative systems; an algebraic approach, Bull. Acad. Polon. des Sci., Ser.sci.math.astronom. et phys., 20 (1971), 51\u201355","journal-title":"Bull. Acad. Polon. des Sci., Ser.sci.math.astronom. et phys."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Blikle, A. An analysis of programs by algebraic means. In: Mathematical Foundations of Comp. Sci. (A.Mazurkiewicz, Ed.), Banach Center Publications, vol.2 (1977), Polish Scientific Publishers, Warsaw 1977","DOI":"10.4064\/-2-1-167-213"},{"key":"2_CR7","unstructured":"Blikle, A. An analytic approach to the verification of iterative programs. Proc. IFIP-1977 Congress, Toronto 1977"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Blikle, A. and Budkowski, S. Certification of microprograms by an algebraic method. Micro-9 Proc., Ninth Annual Workshop on Micro-programming, September 1976, 9\u201314","DOI":"10.1145\/800145.804779"},{"key":"2_CR9","unstructured":"Blikle, A. and Mazurkiewicz, A. An algebraic approach to the theory of programs, algorithms, languages and recursiveness. In: Math. Found. Comp. Sci. (Proc. Warsaw-Jablonna, 1972), Warsaw 1972"},{"key":"2_CR10","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E. A Discipline of Programming. Prentice-Hall, Inc., Englewood Cliffs 1976"},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"R. W. Floyd","year":"1967","unstructured":"Floyd, R.W. Assigning meanings to programs. Proc. Symp. in Applied Math. 19 (1967), 19\u201332","journal-title":"Proc. Symp. in Applied Math."},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. R. Hoare","year":"1969","unstructured":"Hoare, C.A.R. An axiomatic basis for computer programming, Communication of ACM, 12 (1969), 576\u2013583","journal-title":"Communication of ACM"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S. Katz","year":"1976","unstructured":"Katz, S. and Manna, Z. Logical analysis of programs. Communications of ACM, 19 (1976), 188\u2013206","journal-title":"Communications of ACM"},{"key":"2_CR14","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"Kleene, S.C. Introduction to Metamathematics, North-Holland, Amsterdam 1952"},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1145\/365230.365257","volume":"9","author":"P. J. Landin","year":"1966","unstructured":"Landin, P.J. The next 700 programming languages, Communication of ACM, 9 (1966), 157\u2013164","journal-title":"Communication of ACM"},{"key":"2_CR16","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0022-0000(69)80009-7","volume":"3","author":"Z. Manna","year":"1969","unstructured":"Manna, Z. The correctness of programs. J. Comp. Syst. Sci., 3 (1969), 119\u2013127","journal-title":"J. Comp. Syst. Sci."},{"key":"2_CR17","volume-title":"Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z. Mathematical Theory of Computation. McGraw-Hill, New York 1974"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Pnueli, A. Axiomatic approach to total correctness of programs. Acta Informatica (1974)","DOI":"10.1007\/BF00288637"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1016\/S0019-9958(71)90355-X","volume":"18","author":"A. Mazurkiewicz","year":"1971","unstructured":"Mazurkiewicz, A. Proving algorithms by tail functions. Working paper for IFIP WG 2.2. February 1970, since published in Information and Control, 18 (1971), 220\u2013226","journal-title":"Information and Control"},{"key":"2_CR20","first-page":"793","volume":"20","author":"A. Mazurkiewicz","year":"1972","unstructured":"Mazurkiewicz, A. Iteratively computable relations. Bull. Acad. Polon. Sci., Ser.sci.math.astronom. phys., 20 (1972), 793\u2013797","journal-title":"Bull. Acad. Polon. Sci., Ser.sci.math.astronom. phys."},{"key":"2_CR21","first-page":"5","volume":"11","author":"A. Mazurkiewicz","year":"1974","unstructured":"Mazurkiewicz, A. Proving properties of processes. Algorytmy, 11 (1974), 5\u201322","journal-title":"Algorytmy"},{"key":"2_CR22","volume-title":"A Theory of Programming Language Semantics","author":"R. Milne","year":"1977","unstructured":"Milne, R. and Strachey, Ch. A Theory of Programming Language Semantics, Chapman and Hall, London 1977"},{"key":"2_CR23","unstructured":"Morris, F.L. The next 700 programming language description, unpublished manuscript."},{"key":"2_CR24","unstructured":"Mosses, P. The mathematical semantics of ALGOL 60. Technical Monograph PRG-12, Oxford University, 1974"},{"key":"2_CR25","first-page":"59","volume-title":"Machine Intelligence, vol. 5","author":"D. Park","year":"1970","unstructured":"Park, D. Fixpoint induction and proofs of program properties. In: Machine Intelligence, vol. 5 (B. Meltzer and D. Michie eds.), pp.59\u201378. Edinburgh University Press, Edinburgh 1970"},{"key":"2_CR26","first-page":"472","volume-title":"Math. Found. Comp. Sci.","author":"W. P. Roever de","year":"1976","unstructured":"de Roever, W.P. Dijkstra's predicate transformer, non-determinism, recursion and termination. In: Math. Found. Comp. Sci. 1976 (Proc. Symp. Gdansk, 1976, A. Mazurkiewicz, Ed.) Lecture Note in CS, Springer, Berlin, 472\u2013481"},{"key":"2_CR27","unstructured":"Scott, D. and de Bakker, J.W. A theory of programs, unpublished notes, IBM seminar, Vienna 1969"},{"key":"2_CR28","unstructured":"Strachey, C. and Wadsworth, C.P. Continuation, a mathematical semantics for handling full jumps. Technical Monograph PRG-11, Oxford 1974"},{"key":"2_CR29","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A. A lattice-theoretic fixedpoint theorem and its applications. Pacific Journal of Math., 5 (1955), 285\u2013309","journal-title":"Pacific Journal of Math."},{"key":"2_CR30","unstructured":"Turing, A.M. On checking a large routine. Report of a Conference on High Speed Automatic Calculating Machines, pp.67\u201369, University Mathematical Laboratory, Cambridge 1949"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1977"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-08353-7_124.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T20:52:05Z","timestamp":1619556725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-08353-7_124"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1977]]},"ISBN":["9783540083535","9783540372851"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-08353-7_124","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1977]]}}}