{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:38:45Z","timestamp":1725791925069},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_30","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"432-448","source":"Crossref","is-referenced-by-count":6,"title":["Formal Verification of Operational Transformation"],"prefix":"10.1007","author":[{"given":"Yang","family":"Liu","sequence":"first","affiliation":[]},{"given":"Yi","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Shao Jie","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Chengzheng","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"http:\/\/cooffice.ntu.edu.sg\/otfaq\/"},{"key":"30_CR2","unstructured":"http:\/\/pat.sce.ntu.edu.sg\/ot"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-02138-1_5","volume-title":"Formal Techniques for Distributed Systems","author":"H. Boucheneb","year":"2009","unstructured":"Boucheneb, H., Imine, A.: On model-checking optimistic replication algorithms. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS\/FORTE 2009. LNCS, vol.\u00a05522, pp. 73\u201389. Springer, Heidelberg (2009)"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Ellis, C.A., Gibbs, S.J.: Concurrency control in groupware systems. In: SIGMOD, pp. 399\u2013407 (1989)","DOI":"10.1145\/66926.66963"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Imine, A., Molli, P., Oster, G., Rusinowitch, M.: Proving Correctness of Transformation Functions in Real-time Groupware. In: ECSCW, pp. 277\u2013293 (2003)","DOI":"10.1007\/978-94-010-0068-0_15"},{"issue":"7","key":"30_CR6","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1998","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. CACM\u00a021(7), 558\u2013565 (1998)","journal-title":"CACM"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Nichols, D.A., Curtis, P., Dixon, M., Lamping, J.: High-latency, low-bandwidth windowing in the Jupiter collaboration system. In: UIST, pp. 111\u2013120 (1995)","DOI":"10.1145\/215585.215706"},{"issue":"4","key":"30_CR8","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1145\/198425.198427","volume":"1","author":"A. Prakash","year":"1994","unstructured":"Prakash, A., Knister, M.J.: A framework for undoing actions in collaborative systems. TOCHI\u00a01(4), 295\u2013330 (1994)","journal-title":"TOCHI"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Ressel, M., Nitsche-Ruhland, D., Gunzenh\u00e4user, R.: An integrating, transformation-oriented approach to concurrency control and undo in group editors. In: CSCW, pp. 288\u2013297 (1996)","DOI":"10.1145\/240080.240305"},{"issue":"4","key":"30_CR10","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1145\/586081.586085","volume":"9","author":"C. Sun","year":"2002","unstructured":"Sun, C.: Undo as concurrent inverse in group editors. TOCHI\u00a09(4), 309\u2013361 (2002)","journal-title":"TOCHI"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Sun, C., Ellis, C.A.: Operational transformation in real-time group editors: issues, algorithms, and achievements. In: CSCW, pp. 59\u201368 (1998)","DOI":"10.1145\/289444.289469"},{"issue":"1","key":"30_CR12","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/274444.274447","volume":"5","author":"C. Sun","year":"1998","unstructured":"Sun, C., Jia, X., Zhang, Y., Yang, Y., Chen, D.: Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems. TOCHI\u00a05(1), 63\u2013108 (1998)","journal-title":"TOCHI"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Sun, C., Xu, Y., Agustina: Exhaustive search of puzzles in operational transformation. In: CSCW, pp. 519\u2013529 (2014)","DOI":"10.1145\/2531602.2531630"},{"issue":"10","key":"30_CR14","first-page":"1454","volume":"20","author":"D. Sun","year":"2009","unstructured":"Sun, D., Sun, C.: Context-based operational transformation in distributed collaborative editing systems. TPDS\u00a020(10), 1454\u20131470 (2009)","journal-title":"TPDS"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Xu, Y., Sun, C., Li, M.: Achieving convergence in operational transformation: conditions, mechanisms and systems. In: CSCW, pp. 505\u2013518 (2014)","DOI":"10.1145\/2531602.2531629"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T16:33:19Z","timestamp":1558888399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}