{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T18:50:29Z","timestamp":1672339829372},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,8,3]],"date-time":"2006-08-03T00:00:00Z","timestamp":1154563200000},"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,10]]},"DOI":"10.1007\/s00236-006-0020-1","type":"journal-article","created":{"date-parts":[[2006,8,2]],"date-time":"2006-08-02T19:37:22Z","timestamp":1154547442000},"page":"195-222","source":"Crossref","is-referenced-by-count":8,"title":["Refinement verification of the lazy caching algorithm"],"prefix":"10.1007","volume":"43","author":[{"given":"Wim H.","family":"Hesselink","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,8,3]]},"reference":[{"key":"20_CR1","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. (1993). Lazy caching. ACM Trans. Program. Lang. Syst. 15: 182\u2013206","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR2","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. (1991). The existence of refinement mappings. Theor. Comput. Sci. 82: 253\u2013284","journal-title":"Theor. Comput. Sci."},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Arons, T.: Using timestamping and history variables to verify sequential consistency. In Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, 13th International Conference, CAV 2001, Paris, LNCS, vol. 2102\u00a0pp. 223\u2013235 Springer, Berlin Heidelberg New York (2001)","DOI":"10.1007\/3-540-44585-4_42"},{"key":"20_CR4","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s004460050058","volume":"12","author":"E. Brinksma","year":"1999","unstructured":"Brinksma E. (1999). Cache consistency by design. Distrib. Comput. 12: 61\u201374","journal-title":"Distrib. Comput."},{"key":"20_CR5","volume-title":"Parallel Program Design, A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy K.M., Misra J. (1988). Parallel Program Design, A Foundation. Addison\u2013Wesley, Reading"},{"key":"20_CR6","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s004460050057","volume":"12","author":"R. Gerth","year":"1999","unstructured":"Gerth R. (1999). Sequential consistency and the lazy caching algorithm. Distrib. Comput. 12: 57\u201359","journal-title":"Distrib. Comput."},{"key":"20_CR7","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/s004460050059","volume":"12","author":"S. Graf","year":"1999","unstructured":"Graf S. (1999). Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Distrib. Comput. 12: 75\u201390","journal-title":"Distrib. Comput."},{"key":"20_CR8","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\u00a0pp. 187\u2013196. Springer Berlin Heidelberg New York (1986)","DOI":"10.1007\/3-540-16442-1_14"},{"key":"20_CR9","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 pages 117\u2013130. Springer Berlin Heidelberg New York (2002)","DOI":"10.1007\/3-540-45442-X_8"},{"key":"20_CR10","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. (2004). Using eternity variables to specify and prove a serializable database interface. Sci. Comput. Program. 51: 47\u201385","journal-title":"Sci. Comput. Program."},{"key":"20_CR11","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/1042038.1042044","volume":"6","author":"W.H. Hesselink","year":"2005","unstructured":"Hesselink W.H. (2005). Eternity variables to prove simulation of specifications. ACM Trans. Comp. Logic 6: 175\u2013201","journal-title":"ACM Trans. Comp. Logic"},{"key":"20_CR12","unstructured":"Hesselink, W.H.: Universal extensions to simulate specifications. In preparation, see http: www.cs.rug.nl\/~wim\/pub\/mans.html1, 2005"},{"key":"20_CR13","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/s00236-006-0007-y","volume":"42","author":"W.H. Hesselink","year":"2006","unstructured":"Hesselink W.H. (2006). Splitting forward simulations to cope with liveness. Acta Inf. 42: 583\u2013602","journal-title":"Acta Inf."},{"key":"20_CR14","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/s004460050061","volume":"12","author":"W. Janssen","year":"1999","unstructured":"Janssen W., Poel M., Zwiers J. (1999). The compositional approach to sequential consistency and lazy caching. Distrib. Comput. 12: 105\u2013127","journal-title":"Distrib. Comput."},{"key":"20_CR15","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. (1999). Proving refinement using transduction. Distrib. Comput. 12: 129\u2013149","journal-title":"Distrib. Comput."},{"key":"20_CR16","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. (1999). Lazy caching in TLA. Distrib. Comput. 12: 151\u2013174","journal-title":"Distrib. Comput."},{"key":"20_CR17","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/63238.63240","volume":"32","author":"L. Lamport","year":"1989","unstructured":"Lamport L. (1989). A simple approach to specifying concurrent systems. Commun. ACM 32: 32\u201345","journal-title":"Commun. ACM"},{"key":"20_CR18","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport L. (1994). The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16: 872\u2013923","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR19","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/s004460050060","volume":"12","author":"G. Lowe","year":"1999","unstructured":"Lowe G., Davies J. (1999). Using CSP to verify sequential consistency. Distrib. Comput. 12: 91\u2013103","journal-title":"Distrib. Comput."},{"key":"20_CR20","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N. Lynch","year":"1995","unstructured":"Lynch N., Vaandrager F. (1995). Forward and backward simulations, part I: untimed systems. Inf. Comput. 121: 214\u2013233","journal-title":"Inf. Comput."},{"key":"20_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna Z., Pnueli A. (1992). The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin Heidelberg New York"},{"key":"20_CR22","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/s004460050056","volume":"12","author":"M. Meritt","year":"1999","unstructured":"Meritt M. (1999). Introduction. Distrib. Comput. 12: 55\u201356","journal-title":"Distrib. Comput."},{"key":"20_CR23","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of 2nd International Joint Conference on Artificial Intelligence, pp. 481\u2013489. British Comp. Soc., 1971"},{"key":"20_CR24","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Version 2.4, System Guide, Prover Guide, PVS Language Reference, 2001. http:\/\/pvs.csl.sri.com"},{"key":"20_CR25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02276637","volume":"6","author":"F.B. Schneider","year":"1992","unstructured":"Schneider F.B. (1992). Introduction. Distrib. Comput. 6: 1\u20133","journal-title":"Distrib. Comput."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0020-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-006-0020-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0020-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T09:41:53Z","timestamp":1558690913000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-006-0020-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8,3]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["20"],"URL":"https:\/\/doi.org\/10.1007\/s00236-006-0020-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8,3]]}}}