{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T16:05:53Z","timestamp":1771949153046,"version":"3.50.1"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319737201","type":"print"},{"value":"9783319737218","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_17","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T09:13:05Z","timestamp":1514452385000},"page":"358-381","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Co-Design and Verification of an Available File System"],"prefix":"10.1007","author":[{"given":"Mahsa","family":"Najafzadeh","sequence":"first","affiliation":[]},{"given":"Marc","family":"Shapiro","sequence":"additional","affiliation":[]},{"given":"Patrick","family":"Eugster","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"17_CR1","unstructured":"https:\/\/github.com\/Z3Prover\/z3"},{"key":"17_CR2","unstructured":"POSIX.1-2008. The Open Group Base Specifications Issue 7"},{"key":"17_CR3","unstructured":"Google Drive (2017). https:\/\/www.google.com\/drive\/"},{"key":"17_CR4","unstructured":"Microsoft OneDrive (2017). https:\/\/onedrive.live.com\/"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-76650-6_1","volume-title":"Formal Methods and Software Engineering","author":"J-R Abrial","year":"2007","unstructured":"Abrial, J.-R.: A system development process with Event-B and the Rodin platform. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 1\u20133. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-76650-6_1"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-540-30482-1_32","volume-title":"Formal Methods and Software Engineering","author":"K Arkoudas","year":"2004","unstructured":"Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a file system implementation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 373\u2013390. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_32"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Baker, M.G., Hartman, J.H., Kupfer, M.D., Shirriff, K.W., Ousterhout, J.K.: Measurements of a distributed file system. In: Proceedings of the Thirteenth ACM Symposium on Operating Systems Principles, SOSP 1991, pp. 198\u2013212. ACM, New York (1991)","DOI":"10.1145\/121132.121164"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Balasubramaniam, S., Pierce, B.C.: What is a file synchronizer? In: Int. Conf. on Mobile Comp. and Netw. (MobiCom 1998). ACM\/IEEE, October 1998","DOI":"10.1145\/288235.288261"},{"key":"17_CR9","unstructured":"Bernstein, P., Radzilacos, V., Hadzilacos, V.: Concurrency Control and Recovery in Database Systems. Addison Wesley Publishing Company (1987)"},{"issue":"4","key":"17_CR10","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1093\/logcom\/exm019","volume":"17","author":"N Biri","year":"2007","unstructured":"Biri, N., Galmiche, D.: Models and separation logics for resource trees. Journal of Logic and Computation 17(4), 687\u2013726 (2007)","journal-title":"Journal of Logic and Computation"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-75221-9_1","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"N Bj\u00f8rner","year":"2007","unstructured":"Bj\u00f8rner, N.: Models and software model checking of a distributed file replication system. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 1\u201323. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75221-9_1"},{"key":"17_CR12","unstructured":"Carns, P.H., Ligon III, W.B., Ross, R.B., Thakur, R.: PVFS: a parallel file system for linux clusters. In: Proceedings of the 4th Annual Linux Showcase and Conference, ALS 2000, Berkeley, CA, USA, pp. 28\u201328 (2000)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Clements, A.T., Kaashoek, M.F., Zeldovich, N., Morris, R.T., Kohler, E.: The scalable commutativity rule: designing scalable software for multicore processors. In: Symp. on Op. Sys. Principles (SOSP), ACM SIG on Op. Sys. (SIGOPS), pp. 1\u201317. Assoc. for Computing Machinery, Farmington (2013)","DOI":"10.1145\/2517349.2522712"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-88194-0_5","volume-title":"Formal Methods and Software Engineering","author":"K Damchoom","year":"2008","unstructured":"Damchoom, K., Butler, M., Abrial, J.-R.: Modelling and proof of a tree-structured file system in Event-B and Rodin. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 25\u201344. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_5"},{"issue":"3","key":"17_CR15","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1145\/5505.5508","volume":"17","author":"SB Davidson","year":"1985","unstructured":"Davidson, S.B., Garcia-Molina, H., Skeen, D.: Consistency in a partitioned network: a survey. ACM Comput. Surv. 17(3), 341\u2013370 (1985). http:\/\/doi.acm.org\/10.1145\/5505.5508","journal-title":"ACM Comput. Surv."},{"key":"17_CR16","unstructured":"El Ghazi, A.A., Taghdiri, M.: Analyzing alloy constraints using an SMT solver: a case study. In: 5th International Workshop on Automated Formal Methods (AFM), Edinburgh, United Kingdom (2010)"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Freitas, L., Woodcock, J., Butterfield, A.: POSIX and the verification grand challenge: a roadmap. In: Proceedings of the 13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 153\u2013162, March 2008","DOI":"10.1109\/ICECCS.2008.35"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-54833-8_10","volume-title":"Programming Languages and Systems","author":"P Gardner","year":"2014","unstructured":"Gardner, P., Ntzik, G., Wright, A.: Local reasoning for the POSIX file system. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 169\u2013188. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_10"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Ghemawat, S., Gobioff, H., Leung, S.T.: The google file system. In: Symp. on Op. Sys. Principles (SOSP), pp. 29\u201343. Assoc. for Computing Machinery, Bolton Landing, October 2003","DOI":"10.1145\/945445.945450"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Yang, H., Ferreira, C., Najafzadeh, M., Shapiro, M.: \u2018Cause I\u2019m strong enough: reasoning about consistency choices in distributed systems. In: Symp. on Principles of Prog. Lang. (POPL). St. Petersburg, FL (2016)","DOI":"10.1145\/2837614.2837625"},{"key":"17_CR21","unstructured":"Guy, R., Heidemann, J.S., Mak, W., Popek, G.J., Rothmeier, D.: Implementation of the ficus replicated file system. In: USENIX Conference Proceedings, pp. 63\u201371 (1990)"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Haogang, C., Daniel, Z., Tej, C., Adam, C., Frans, K.M., Nickolai, Z.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, pp. 18\u201337. ACM, New York (2015)","DOI":"10.1145\/2815400.2815402"},{"issue":"1","key":"17_CR23","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s00165-010-0171-2","volume":"24","author":"WH Hesselink","year":"2010","unstructured":"Hesselink, W.H., Lali, M.: Formalizing a hierarchical file system. Formal Aspects of Computing 24(1), 27\u201344 (2010)","journal-title":"Formal Aspects of Computing"},{"key":"17_CR24","unstructured":"Hughes, J.: Specifying a visual file system in z. In: IEEE Colloquium on Formal Methods in HCI: II, pp. 3\/1-3\/3, December 1989"},{"key":"17_CR25","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, North-Holland (1983)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Kistler, J.J., Satyanarayanan, M.: Disconnected operation in the Coda file system. In: Symp. on Principles of Dist. Comp. (PODC), vol. 10, pp. 3\u201325, February 1992","DOI":"10.1145\/146941.146942"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Kumar, P., Satyanarayanan, M.: Flexible and safe resolution of file conflicts. In: Usenix Tech. Conf., New Orleans, LA, USA, January 1995","DOI":"10.21236\/ADA289342"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-27940-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"KRM Leino","year":"2012","unstructured":"Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315\u2013331. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_21"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Morgan, C., Sufrin, B.: Specification of the UNIX filing system, vol. SE-10, pp. 128\u2013142 (1984)","DOI":"10.1109\/TSE.1984.5010215"},{"key":"17_CR30","unstructured":"Nadkarni, A.: Scale-out file systems on object-based storage platforms. IDC Technology Assessment 258393, International Data Corporation (IDC), Framingham, MA, USA (2015)"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Najafzadeh, M., Gotsman, A., Yang, H., Ferreira, C., Shapiro, M.: The CISE tool: proving weakly-consistent applications correct. In: W. on Principles and Practice of Consistency for Distributed Data (PaPoC). EuroSys 2016 workshops, ACM SIG on Op. Sys. (SIGOPS). Assoc. for Computing Machinery, London, April 2016","DOI":"10.1145\/2911151.2911160"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Ntzik, G., Gardner, P.: Reasoning about the POSIX file system: local update and global pathnames. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pp. 201\u2013220. ACM, New York (2015)","DOI":"10.1145\/2814270.2814306"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Ousterhout, J.K., Da Costa, H., Harrison, D., Kunze, J.A., Kupfer, M., Thompson, J.G.: A trace-driven analysis of the UNIX 4.2 BSD file system. In: SIGOPS Oper. Syst. Rev., vol. 19, pp. 15\u201324. ACM, New York, December 1985","DOI":"10.1145\/323647.323631"},{"key":"17_CR34","unstructured":"Pawlowski, B., Juszczak, C., Staubach, P., Smith, C., Lebel, D., Hitz, D.: NFS version 3 design and implementation. In: Proceedings of the Summer 1994 USENIX Technical Conference, pp. 137\u2013152 (1994)"},{"key":"17_CR35","doi-asserted-by":"crossref","unstructured":"Petersen, K., Spreitzer, M.J., Terry, D.B., Theimer, M.M., Demers, A.J.: Flexible update propagation for weakly consistent replication. In: Symp. on Op. Sys. Principles (SOSP), pp. 288\u2013301. ACM SIGOPS, Saint Malo, October 1997","DOI":"10.1145\/268998.266711"},{"key":"17_CR36","unstructured":"Ramsey, N., Csirmaz, E.: An algebraic approach to file synchronization. Tech. Rep. TR-05-01, Harvard University Dept. of Computer Science, Cambridge MA, USA, May 2001"},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, pp. 55\u201374. IEEE Computer Society, Washington, DC (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"17_CR38","unstructured":"Sandberg, R., Goldberg, D., Kleiman, S., Walsh, D., Lyon, B.: Design and implementation of the Sun Network Filesystem. In: Summer 1985 USENIX Conf. pp. 119\u2013130. USENIX, Portland, June 1985"},{"key":"17_CR39","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1109\/12.54838","volume":"39","author":"M Satyanarayanan","year":"1990","unstructured":"Satyanarayanan, M., Kistler, J.J., Kumar, P., Okasaki, M.E., Siegel, E.H., Steere, D.C.: Coda: A highly available file system for a distributed workstation environment. IEEE Trans. on Computers. 39, 447\u2013459 (1990)","journal-title":"IEEE Trans. on Computers."},{"key":"17_CR40","unstructured":"Schmuck, F., Haskin, R.: GPFS: a shared-disk file system for large computing clusters. In: Proceedings of the 1st USENIX Conference on File and Storage Technologies, FAST 2002. USENIX Association, Berkeley (2002)"},{"key":"17_CR41","unstructured":"Schwan, P.: Lustre: Building a file system for 1,000-node clusters. In: Proceedings of the 2003 Linux Symposium (2003)"},{"key":"17_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-24550-3_29","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"M Shapiro","year":"2011","unstructured":"Shapiro, M., Pregui\u00e7a, N., Baquero, C., Zawirski, M.: Conflict-free replicated data types. In: D\u00e9fago, X., Petit, F., Villain, V. (eds.) SSS 2011. LNCS, vol. 6976, pp. 386\u2013400. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24550-3_29"},{"key":"17_CR43","doi-asserted-by":"crossref","unstructured":"Shvachko, K., Kuang, H., Radia, S., Chansler, R.: The hadoop distributed file system. In: Proceedings of the 2010 IEEE 26th Symposium on Mass Storage Systems and Technologies (MSST), MSST 2010, pp. 1\u201310. IEEE Computer Society, Washington, DC (2010)","DOI":"10.1109\/MSST.2010.5496972"},{"key":"17_CR44","unstructured":"Spivey, J.M.: The z notation: a reference manual. In: Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems (1998)"},{"key":"17_CR45","doi-asserted-by":"crossref","unstructured":"Tao, V., Shapiro, M., Rancurel, V.: Merging semantics for conflict updates in geo-distributed file systems. In: ACM Int. Systems and Storage Conf. (Systor), Haifa, Israel, pp. 10.1-10.12, May 2015","DOI":"10.1145\/2757667.2757683"},{"key":"17_CR46","doi-asserted-by":"crossref","unstructured":"Thekkath, C.A., Mann, T., Lee, E.K.: Frangipani: a scalable distributed file system. In: SIGOPS Oper. Syst. Rev. vol. 31, pp. 224\u2013237. ACM, New York, October 1997","DOI":"10.1145\/268998.266694"},{"key":"17_CR47","doi-asserted-by":"crossref","unstructured":"Vogels, W.: File system usage in windows nt 4.0. In: Proceedings of the Seventeenth ACM Symposium on Operating Systems Principles (SOSP), pp. 93\u2013109. ACM, New York (1999)","DOI":"10.1145\/319151.319158"},{"key":"17_CR48","doi-asserted-by":"crossref","unstructured":"Vogels, W.: Eventually consistent. In: ACM Queue, vol. 6, pp. 14\u201319, October 2008","DOI":"10.1145\/1466443.1466448"},{"key":"17_CR49","doi-asserted-by":"crossref","unstructured":"Wang, A.I., Reiher, P., Bagrodia, R., Kuenning, G.: Understanding the behavior of the conflict-rate metric in optimistic peer replication. In: Proceedings of the 13th International Workshop on Database and Expert Systems Applications, pp. 757\u2013761, September 2002","DOI":"10.1109\/DEXA.2002.1045989"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,29]],"date-time":"2025-06-29T08:23:53Z","timestamp":1751185433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}