{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T17:10:11Z","timestamp":1683393011369},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"8-9","license":[{"start":{"date-parts":[[2006,3,1]],"date-time":"2006-03-01T00:00:00Z","timestamp":1141171200000},"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":[[2006,4,7]]},"DOI":"10.1007\/s00236-006-0007-y","type":"journal-article","created":{"date-parts":[[2006,2,28]],"date-time":"2006-02-28T14:08:29Z","timestamp":1141135709000},"page":"583-602","source":"Crossref","is-referenced-by-count":9,"title":["Splitting forward simulations to copewith liveness"],"prefix":"10.1007","volume":"42","author":[{"given":"Wim H.","family":"Hesselink","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,3,1]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82, 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR2","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1145\/151646.151651","volume":"15","author":"Y. Afek","year":"1993","unstructured":"Afek, Y., Brown, G., Merrit, M.: Lazy caching. ACM Trans. Program Lang. Syst. 15, 182\u2013206 (1993)","journal-title":"ACM Trans. Program Lang. Syst."},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: A class of allocation strategies inducing bounded delays only. Technical Report, Technical University Eindhoven, EWD 319, see www.cs.utexas.edu\/users\/EWD (1971)","DOI":"10.1145\/1478873.1478997"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 86, LNCS, vol. 213, Springer, New York, pp. 187\u2013196 (1986)","DOI":"10.1007\/3-540-16442-1_14"},{"key":"7_CR5","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(88)90143-0","volume":"59","author":"W.H. Hesselink","year":"1988","unstructured":"Hesselink, W.H.: Deadlock and fairness in morphisms of transition systems. Theor. Comput. Sci. 59, 235\u2013257 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Hesselink, W.H.: Eternity variables to simulate specifications. In: Boiten, E.A., Moeller, B. (eds.) MPC 2002, LNCS, vol. 2386, Springer, New York, pp. 117\u201330 (2002)","DOI":"10.1007\/3-540-45442-X_8"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Hesselink, W.H.: Refinement verification of the lazy caching algorithm. manuscript in preparation, see http:\/\/www.cs.rug.nl\/\u223cwim\/pub\/mans.html (2006)","DOI":"10.1007\/s00236-006-0020-1"},{"key":"7_CR8","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.scico.2003.06.001","volume":"51","author":"W.H. Hesselink","year":"2004","unstructured":"Hesselink, W.H.: Using eternity variables to specify and prove a serializable database interface. Sci. Comput. Program 51, 47\u201385 (2004)","journal-title":"Sci. Comput. Program"},{"key":"7_CR9","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/1042038.1042044","volume":"6","author":"W.H. Hesselink","year":"2005","unstructured":"Hesselink, W.H.: Eternity variables to prove simulation of specifications. ACM Trans. Comp. Logic 6, 175\u2013201 (2005)","journal-title":"ACM Trans. Comp. Logic"},{"key":"7_CR10","unstructured":"Hesselink, W.H.: Universal extensions to simulate specifications. Manuscript in preparation, see www.cs.rug.nl\/ wim\/pub\/mans.html (2005)"},{"key":"7_CR11","first-page":"346","volume-title":"Simulations between specifications of distributed systems","author":"B. Jonnson","year":"1991","unstructured":"Jonnson, B.: Simulations between specifications of distributed systems. In: Baeten, J.C.M., Groote, J.F. (eds.) CONCUR \u201891, LNCS, vol. 527, Springer, New York, pp. 346\u2013360 (1991)"},{"key":"7_CR12","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/s004460050062","volume":"12","author":"B. Jonsson","year":"1999","unstructured":"Jonsson, B., Pnueli, A., Rump, C.: Proving refinement using transduction. Distr. Comput. 12, 129\u2013149 (1999)","journal-title":"Distr. Comput."},{"key":"7_CR13","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s004460050063","volume":"12","author":"P. Ladkin","year":"1999","unstructured":"Ladkin, P., Lamport, L., Olivier, B., Roegel, D.: Lazy caching inTLA. Distr. Comput. 12, 151\u2013174 (1999)","journal-title":"Distr. Comput."},{"key":"7_CR14","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/63238.63240","volume":"32","author":"L. Lamport","year":"1989","unstructured":"Lamport, L.: A simple approach to specifying concurrent systems. Commun. ACM 32, 32\u201345 (1989)","journal-title":"Commun. ACM"},{"key":"7_CR15","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1080\/00029890.1995.12004627","volume":"102","author":"L. Lamport","year":"1993","unstructured":"Lamport, L.: How to write a proof. Am. Math. Month. 102, 600\u2013608 (1993)","journal-title":"Am. Math. Month."},{"key":"7_CR16","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program Lang. Syst. 16, 872\u2013923 (1994)","journal-title":"ACM Trans. Program Lang. Syst."},{"key":"7_CR17","first-page":"214","volume":"121","author":"N. Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations. Part I: Untimed systems. Inf. Comput. 121, 214\u2013233 (1995)","journal-title":"Part I: Untimed systems. Inf. Comput."},{"key":"7_CR18","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence, British Computer Society 1971, pp. 481\u2013489"},{"key":"7_CR19","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Inf. 6, 319\u2013340 (1976)","journal-title":"Acta Inf."},{"key":"7_CR20","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Version 2.4, System Guide, Prover Guide, PVS Language Reference, http:\/\/pvs.csl.sri.com (2001)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0007-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-006-0007-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0007-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,6]],"date-time":"2023-05-06T16:33:48Z","timestamp":1683390828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-006-0007-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,1]]},"references-count":20,"journal-issue":{"issue":"8-9","published-print":{"date-parts":[[2006,4,7]]}},"alternative-id":["7"],"URL":"https:\/\/doi.org\/10.1007\/s00236-006-0007-y","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,3,1]]}}}