{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T03:50:36Z","timestamp":1648957836400},"publisher-location":"Berlin\/Heidelberg","reference-count":22,"publisher":"Springer-Verlag","isbn-type":[{"value":"0387973753","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0040269","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T17:01:43Z","timestamp":1155834103000},"page":"373-389","source":"Crossref","is-referenced-by-count":0,"title":["Does \u201cN+1 times\u201d prove more programs correct than \u201cN times\u201d?"],"prefix":"10.1007","author":[{"given":"Ana","family":"Pasztor","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"H. Andr\u00e9ka, Sharpening the characterization of the power of Floyd's method, in: Logic of Programs and their Applications, ed.: A. Salwicki (Proc. Conf. Poznan 1980), Lecture Notes in Computer Science 148, Springer-Verlag 2983, pp. 1\u201326.","DOI":"10.1007\/3-540-11981-7_1"},{"key":"18_CR2","unstructured":"H. Andr\u00e9ka, K. Balogh, K. L\u00e1badi, I. N\u00e9meti, P. T\u00f3th, Plan for improving a working program verifier program, Software Dept. of Computing Center of the Heavy Industries, Preprint 1974, Budapest (in Hungarian)."},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1016\/0304-3975(82)90004-4","volume":"17","author":"H. Andr\u00e9ka","year":"1982","unstructured":"H. Andr\u00e9ka, I. N\u00e9meti and I. Sain, A complete logic for reasoning about programs via nonstandard model theory, Parts I-II, Theoretical Computer Science 17 (1982), pp. 193\u2013212 and pp. 259\u2013278.","journal-title":"Theoretical Computer Science"},{"key":"18_CR4","unstructured":"R.M. Burstall, Program proving as hand simulation with a little induction, IFIP Congress, Stockholm, August 3\u201310, 1974."},{"key":"18_CR5","first-page":"219","volume":"34","author":"J. Clifford","year":"1966","unstructured":"J. Clifford,Tense logi and the logic of change, Logique et Analyse 34 (1966), pp 219\u2013230.","journal-title":"Logique et Analyse"},{"key":"18_CR6","first-page":"443","volume":"42","author":"P. H\u00e1jek","year":"1986","unstructured":"P. H\u00e1jek, Some conservativeness results for nonstandard dynamic logic, in: Algebra, Combinatronics and Logic in Computer Science, eds.: J. Demetrovics, G. Katona, A. Salomaa (Proc. conf. Gy\u0151r Hungary 1983) Colloq. Math. Soc. J. Bolyai Vol. 42, North-Holland, 1986, pp. 443\u2013449.","journal-title":"Colloq. Math. Soc. J. Bolyai"},{"key":"18_CR7","unstructured":"J.A. Makowsky and I. Sain, On the equivalence of weak second order and non-standard time semantics for various program verification systems, Proceedings of the first annual IEEE Symposium on Logic in Computer Science, Cambridge, MA, June 1986, pp. 293\u2013300."},{"key":"18_CR8","unstructured":"J.A. Makowsky and I. Sain, Weak second order characterizations of various program verification systems, Technical Report #457, Technion-Israel Institute of Technology, Comp. Sci. Dept., June 1987. Submitted to Theoretical Computer Science."},{"key":"18_CR9","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-09510-1_31","volume":"71","author":"Z. Manna","year":"1979","unstructured":"Z. Manna and A. Pnueli, The modal logic of programs, in: International Colloquium on Automata, Languages and Programming '79, Graz, Lecture Notes in Computer Science 71, Springer-Verlag, 1979, pp. 385\u2013409.","journal-title":"Graz, Lecture Notes in Computer Science"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BFb0025789","volume":"131","author":"I. N\u00e9meti","year":"1982","unstructured":"I. N\u00e9meti, Nonstandard dynamic logic, in: Logics of Programs, ed.: D. Kozen, (Proc. Conf. New York 1981) Lecture Notes in Computer Science 131, Springer-Verlag, 1982, pp. 311\u2013348.","journal-title":"Lecture Notes in Computer Science"},{"key":"18_CR11","unstructured":"A. Pasztor, Recursive programs and denotational semantics in absolute logics of programs. Technical Report of Florida International University, School of Comp. Sci., #FIU-SCS-87-1, to appear in Theoretical Computer Science."},{"key":"18_CR12","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0747-7171(86)80013-X","volume":"2","author":"A. Pasztor","year":"1986","unstructured":"A. Pasztor, Nonstandard Algorithmic and Dynamic Logic, in: J. Symbolic Computation 2 (1986), pp. 59\u201381.","journal-title":"J. Symbolic Computation"},{"key":"18_CR13","unstructured":"A. Pasztor, An Infinite Hierarchy of Program Verification Methods, Proceedings of Workshop on Many-Sorted Logic and its Applications in Computer Science, Sept., 12\u201314, 1988, Leeds, England, Academic Press (ed. J.V. Tucker), to appear."},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli, The temporal semantics of concurrent programs, Theoretical Computer Science 13 (1981) pp. 45\u201360.","journal-title":"Theoretical Computer Science"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46\u201357. Revised version: Preprint of the Weizman Institute of Science, May 1981.","DOI":"10.1109\/SFCS.1977.32"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"A.N. Prior, Past, present and future, Oxford University Press, 1967.","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001"},{"key":"18_CR17","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1002\/malq.19840303102","volume":"3","author":"I. Sain","year":"1984","unstructured":"I. Sain, Structured nonstandard dynamic logic, Zeitschrift f\u00fcr Math. Logic und Grundlagen der Math. Heft 3, 1984, pp. 481\u2013497.","journal-title":"Logic und Grundlagen der Math"},{"key":"18_CR18","unstructured":"I. Sain, Relative program verifying powers of the various temporal logics, Information and Control, to appear. An extended abstract of this is [19]."},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"I. Sain, The reasoning powers of Burstall's (modal logic) and Pnueli's (temporal logic) program verification methods, in: Logics of Programs, ed.: R. Parikh (Proc. Conf. Brooklyn USA 1985) Lecture Notes in Computer Science 193, Springer-Verlag, pp. 302\u2013319.","DOI":"10.1007\/3-540-15648-8_24"},{"key":"18_CR20","volume-title":"Dynamic logic with nonstandard model theory","author":"I. Sain","year":"1986","unstructured":"I. Sain, Dynamic logic with nonstandard model theory, Dissertation, Hungarian Academy of Sciences, Budapest, 1986 (in Hungarian)."},{"key":"18_CR21","unstructured":"I. Sain, Is \u201cSOME OTHER TIME\u201d sometimes better than \u201cSOMETIME\u201d in proving partial correctness of programs?, to appear in a special vol. of Studia Logica on nonstandard methods edited by M.M. Richter and M.E. Szabo."},{"key":"18_CR22","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1111\/j.1755-2567.1967.tb00609.x","volume":"33","author":"K. Segerberg","year":"1967","unstructured":"K. Segerberg, On the logic of tomorrow, Theoria 33 (1967), pp 45\u201352.","journal-title":"Theoria"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Programming Semantics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0040269.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:40:00Z","timestamp":1607550000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0040269"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["0387973753"],"references-count":22,"URL":"http:\/\/dx.doi.org\/10.1007\/bfb0040269","relation":{}}}