{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:36Z","timestamp":1775790696120,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548321","type":"print"},{"value":"9783642548338","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54833-8_10","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:37:17Z","timestamp":1395394637000},"page":"169-188","source":"Crossref","is-referenced-by-count":18,"title":["Local Reasoning for the POSIX File System"],"prefix":"10.1007","author":[{"given":"Philippa","family":"Gardner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gian","family":"Ntzik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Wright","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Filesystem Hierarchy Standard Group. Filesystem hierarchy standard"},{"key":"10_CR2","unstructured":"POSIX.1-2008, IEEE 1003.1-2008, The Open Group Base Specifications Issue 7"},{"key":"10_CR3","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/j.entcs.2005.11.059","volume":"155","author":"Variables as resource in separation logic","year":"2006","unstructured":"Variables as resource in separation logic. Electronic Notes in Theoretical Computer Science\u00a0155, 247\u2013276 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10_CR4","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.\u00a03308, pp. 373\u2013390. Springer, Heidelberg (2004)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. SIGPLAN Not. (2005)","DOI":"10.1145\/1040305.1040328"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 504\u2013528. Springer, Heidelberg (2010)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Fisher, K., Foster, N., Walker, D., Zhu, K.Q.: Forest: a language and toolkit for programming with filestores. In: ICFP (2011)","DOI":"10.1145\/2034773.2034814"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z\/Eves: an experiment in the verified software repository. In: IEEE International Conference on Engineering of Complex Computer Systems (2007)","DOI":"10.1109\/ICECCS.2007.36"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Freitas, L., Woodcock, J., Butterfield, A.: POSIX and the verification grand challenge: A roadmap. In: ICECCS (2008)","DOI":"10.1109\/ICECCS.2008.35"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Gardner, P., Ntzik, G., Wright, A.: Local Reasoning for the POSIX File System. Technical report, Imperial College London (2014), \n                    \n                      http:\/\/www.doc.ic.ac.uk\/~gn408\/POSIXFS\/","DOI":"10.1007\/978-3-642-54833-8_10"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Gardner, P., Raad, A., Wheelhouse, M., Wright, A.: Abstract Local Reasoning for Concurrent Libraries. In preparation (2014)","DOI":"10.1016\/j.entcs.2014.10.009"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Gardner, P., Smith, G., Wheelhouse, M., Zarfaty, U.: Local Hoare reasoning about DOM. In: PODS (2008)","DOI":"10.1145\/1376916.1376953"},{"key":"10_CR14","unstructured":"Gardner, P., Wheelhouse, M.: Small specifications for tree update, \n                    \n                      http:\/\/www.doc.ic.ac.uk\/~pg\/papers\/move.pdf"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Hesselink, W.H., Lali, M.: Formalizing a hierarchical file system. In: REFINE (2009)","DOI":"10.1016\/j.entcs.2009.12.018"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: POPL (2013)","DOI":"10.1145\/2429069.2429131"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Form. Asp. Comput. (2007)","DOI":"10.1007\/978-3-540-69149-5_6"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Morgan, C., Sufrin, B.: Specification of the UNIX Filing System. IEEE Transactions on Software Engineering (1984)","DOI":"10.1109\/TSE.1984.5010215"},{"key":"10_CR19","unstructured":"Ntzik, G.: Local Reasoning about File Systems. PhD thesis (expected, 2014)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"10_CR21","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"10_CR22","unstructured":"Smith, G.: Local Reasoning about Web Programs. PhD thesis (2011)"},{"key":"10_CR23","series-title":"LNCS","first-page":"149","volume-title":"ESOP 2014","author":"K. Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol.\u00a08410, pp. 149\u2013168. Springer, Heidelberg (2014)"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP (2013)","DOI":"10.1145\/2500365.2500600"},{"key":"10_CR25","unstructured":"Wright, A.: Structural Separation Logic. PhD thesis, Imperial College London (2013)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54833-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T12:21:44Z","timestamp":1558873304000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54833-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548321","9783642548338"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54833-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}