{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:26:48Z","timestamp":1774837608174,"version":"3.50.1"},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1987,2,1]],"date-time":"1987-02-01T00:00:00Z","timestamp":539136000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1987,2]]},"DOI":"10.1007\/bf00290704","type":"journal-article","created":{"date-parts":[[2004,10,5]],"date-time":"2004-10-05T06:39:30Z","timestamp":1096958370000},"page":"1-31","source":"Crossref","is-referenced-by-count":9,"title":["Sometime = always + recursion ? always on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs"],"prefix":"10.1007","volume":"24","author":[{"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","first-page":"51","volume-title":"Proc. 7th ICALP, LNCS 85","author":"R.J. Back","year":"1980","unstructured":"Back, R.J.: Semantics of unbounded nondeterminism, in Proc. 7th ICALP, LNCS 85, pp. 51?63. Berlin, Heidelberg, New York: Springer 1980"},{"key":"CR2","first-page":"308","volume-title":"Information Processing 74","author":"R.M. Burstall","year":"1974","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. Information Processing 74, pp. 308?312. Amsterdam: North-Holland 1974"},{"key":"CR3","first-page":"75","volume-title":"Tools and notions for program construction","author":"P. Cousot","year":"1982","unstructured":"Cousot, P., Cousot, R.: Induction principles for proving invariance properties of programs. In: Tools and notions for program construction. (D. Neel, ed.), pp. 75?119. Cambridge: University Press 1982"},{"key":"CR4","first-page":"277","volume-title":"Algebraic methods in semantics","author":"P. Cousot","year":"1985","unstructured":"Cousot, P., Cousot, R.: ?A la Floyd? induction principles for proving inevitability properties of programs. In: Algebraic methods in semantics. (M. Nivat, J.C. Reynolds, eds.), pp. 277?312. Cambridge: University Press 1985"},{"key":"CR5","series-title":"Research Report LRIM-83-08","volume-title":"?A la Burstall? induction principles for proving inevitability properties of programs","author":"P. Cousot","year":"1983","unstructured":"Cousot, P., Cousot, R.: ?A la Burstall? induction principles for proving inevitability properties of programs, Research Report LRIM-83-08, Univ. of Metz, France, 1983"},{"key":"CR6","volume-title":"A sequel to EWD 592, EWD 600","author":"E.W. Dijkstra","year":"1977","unstructured":"Dijkstra, E.W.: A sequel to EWD 592, EWD 600, Burroughs Corp., Nuemen, The Netherlands 1977"},{"key":"CR7","first-page":"19","volume-title":"Proc. Symp. Appl. Math., 19","author":"R. Floyd","year":"1967","unstructured":"Floyd, R.: Assigning meaning to programs. In: Proc. Symp. Appl. Math., 19. (Schwartz J.T. (ed.)), Am. Math. Soc., pp. 19?32, Providence, 1967"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357073.357080","volume":"1","author":"D. Gries","year":"1979","unstructured":"Gries, D.: Is SOMETIME ever better than ALWAYS? ACM TOPLAS, 1, 258?265 (1979)","journal-title":"ACM TOPLAS"},{"key":"CR9","first-page":"371","volume":"19","author":"R.M. Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs, 19, 371?384 (1976)","journal-title":"Formal verification of parallel programs"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs, IEEE Trans. Soft. Eng., 3, 125?143 (1977)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"CR11","first-page":"141","volume":"10","author":"Z. Manna","year":"1983","unstructured":"Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language, ACM POPL, 10, 141?154 (1983)","journal-title":"ACM POPL"},{"key":"CR12","first-page":"159","volume":"21","author":"Z. Manna","year":"1978","unstructured":"Manna, Z., Waldinger, R.: Is SOMETIME sometimes better than ALWAYS? Intermittent assertions in proving program correctness, 21, 159?172 (1978)","journal-title":"Intermittent assertions in proving program correctness"},{"key":"CR13","volume-title":"Introduction to set theory","author":"J.D. Monk","year":"1969","unstructured":"Monk, J.D.: Introduction to set theory, New York: McGraw-Hill 1969"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM TOPLAS 4, 455?495 (1982)","journal-title":"ACM TOPLAS"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00290704.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00290704\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00290704","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T21:15:40Z","timestamp":1554758140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00290704"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,2]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1987,2]]}},"alternative-id":["BF00290704"],"URL":"https:\/\/doi.org\/10.1007\/bf00290704","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1987,2]]}}}