{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:53:55Z","timestamp":1725663235768},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540156482"},{"type":"electronic","value":"9783540395270"}],"license":[{"start":{"date-parts":[[1985,1,1]],"date-time":"1985-01-01T00:00:00Z","timestamp":473385600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_24","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:21:25Z","timestamp":1330176085000},"page":"302-319","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["The reasoning powers of Burstall's (modal logic) and Pnueli's (temporal logic) program verification methods"],"prefix":"10.1007","author":[{"given":"I.","family":"Sain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"24_CR1","unstructured":"Andr\u00e9ka,H. Balogh,K. L\u00e1badi,K. N\u00e9meti,I. T\u00f3th,P.: Plans to improve our program verifyer program. (In Hungarian). Working paper, NIM IG\u00dcSZI, Dept. of Software Techniques, Budapest, 1974."},{"key":"24_CR2","unstructured":"Andr\u00e9ka,H. N\u00e9meti,I. Sain,I.: A complete first order logic. Preprint Math.Inst.Hung.Acad.Sci. 124 p."},{"issue":"2","key":"24_CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0304-3975(82)90004-4","volume":"17","author":"H. Andr\u00e9ka","year":"1982","unstructured":"Andr\u00e9ka, H. N\u00e9meti, I. Sain, I.: A complete logic for reasoning about programs via nonstandard model theory, Parts I\u2013II. Theoretical Computer Science 17 (1982), No.2 193\u2013212, No.3 259\u2013278.","journal-title":"Theoretical Computer Science"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Bowen,K.A.: Model theory for modal logic (Kripke models for modal predicate calculi). Synthese Library Vol 127, Reidel Publ. Co., 1979.","DOI":"10.1007\/978-94-015-7642-0"},{"key":"24_CR5","unstructured":"Burstall,R.M.: Program Proving as Hand Simulation with a Little Induction. IFIP Congress, Stockholm, August 3\u201310, 1974."},{"issue":"2","key":"24_CR6","first-page":"181","volume":"5","author":"L. Csirmaz","year":"1981","unstructured":"Csirmaz, L.: On the completeness of proving partial correctness. Acta Cybernetica, Tom 5, Fasc 2, Szeged, 1981, 181\u2013190.","journal-title":"Acta Cybernetica"},{"key":"24_CR7","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0304-3975(81)90076-1","volume":"16","author":"L. Csirmaz","year":"1981","unstructured":"Csirmaz, L.: Programs and program verification in a general setting. Theoretical Computer Science 16 (1981) 199\u2013210.","journal-title":"Theoretical Computer Science"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Csirmaz,L.: On the Strength of \"Sometime\" and \"Always\" in Program Verification. Information and Control, vol 57, Nos 2\u20133, 1983.","DOI":"10.1016\/S0019-9958(83)80042-4"},{"issue":"1","key":"24_CR9","first-page":"45","volume":"4","author":"T. Gergely","year":"1978","unstructured":"Gergely, T. Sz\u0151ts, M.: On the incompleteness of proving partial correctness. Acta Cybernetica, Tom 4, Fasc 1, Szeged, 1978, 45\u201357.","journal-title":"Acta Cybernetica"},{"key":"24_CR10","unstructured":"Gergely,T. Ury,L.: Time models for programming logics. In: Mathematical Logic in Computer Science (Proc.conf. Salg\u00f3tarj\u00e1n 1978) Eds.: B.D\u00f6m\u00f6lki, T.Gergely, Colloq.Math.Soc.J.Bolyai vol 26, North-Holland, 1981, 359\u2013427."},{"key":"24_CR11","unstructured":"Manna,Z. Pnueli,A.: The Modal Logic of Programs. Preprint CS81-12, June 1981."},{"key":"24_CR12","unstructured":"Mirkowska,G.: Multimodal logics. Preprint, Institute of Math., Warsaw University."},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BFb0025789","volume-title":"Logics of Programs","author":"I. N\u00e9meti","year":"1982","unstructured":"N\u00e9meti, I.: Nonstandard Dynamic Logic. In: Logics of Programs, Ed.: D. Kozen (Proc.Conf. New York 1981) Lecture Notes in Computer Science 131, Springer-Verlag, Berlin, 1982, 311\u2013348."},{"key":"24_CR14","unstructured":"Pnueli,A.: The Temporal Logic of Programs. Preprint Weitzmann Institute of Science, Dept. of Applied Math., May 1981."},{"key":"24_CR15","volume-title":"Nonstandard Computation Theory","author":"M.M. Richter","year":"1983","unstructured":"Richter, M.M. Szabo, M.E.: Nonstandard Computation Theory. Preprint, Concordia University, Montreal, 1983."},{"key":"24_CR16","unstructured":"Sain,I.: Successor axioms for time increase the program verifying power of full computational induction. Preprint No 23\/1983, Math.Inst.Hung.Acad.Sci., Budapest, 1983."},{"key":"24_CR17","unstructured":"Sain,I.: Model theoretic characterization of Pnueli's temporal program verification method. Manuscript, 1983."},{"key":"24_CR18","unstructured":"Sain,I.: How to define the meaning of iteration ? and Sharpening the characterization of Pnueli's program verification method (Structured NDL Parts II\u2013III). Preprint No 48\/1984, Math.Inst.Hung.Acad.Sci., Budapest, 1984."},{"key":"24_CR19","unstructured":"Sain,I.: Total correctness in nonstandard dynamic logic. Preprint No 8\/1983, Math.Inst.Hung.Acad.Sci., Budapest, 1983."},{"key":"24_CR20","unstructured":"Szabo,M.E.: Personal communication, 1981."},{"key":"24_CR21","unstructured":"Pasztor,A.: Nonstandard Dynamic Logic to Prove Standard Properties of Programs. Carnegie-Mellon Univ., Dept. of Math., Research Report 84-3."},{"key":"24_CR22","unstructured":"Pasztor,A.: Nonstandard Logics of Programs. Carnegie-Mellon Univ. Dept. of Math., Research Report, Dec. 1984."},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Sain,I.: A simple proof for the completeness of Floyd's method. Theoretical Computer Science vol 35, 1985, to appear.","DOI":"10.1016\/0304-3975(85)90024-6"},{"key":"24_CR24","unstructured":"Sain,I.: The implicit information content of Burstall's (modal) program verification method. Preprint No 57\/1984, Math.Inst.Hung.Acad.Sci., Budapest, 1984."},{"key":"24_CR25","unstructured":"Bir\u00f3,B. Sain,I.: Peano Arithmetic for the Time Scale of Nonstandard Logics of Programs. Preprint, 1985."}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T18:18:38Z","timestamp":1578507518000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_24"}},"subtitle":["An application of model theory"],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1985]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}