{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T13:01:50Z","timestamp":1748350910632,"version":"3.37.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_25","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"375-390","source":"Crossref","is-referenced-by-count":7,"title":["Modular Verification of Order-Preserving Write-Back Caches"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"first","affiliation":[]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Bodenm\u00fcller","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"25_CR1","unstructured":"The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2013 edn. The IEEE and The Open Group (2013)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Amani, S., Murray, T.: Specifying a realistic file system. In: Proceedings of Workshop on Models for Formal Analysis of Real Systems. Electronic Proceedings in Theoretical Computer Science, vol. 196, pp. 1\u20139. Open Publishing Association (2015)","DOI":"10.4204\/EPTCS.196.1"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Kaufmann, A., Li, J., Krishnamurthy, A., Torlak, E., Wang, X.: Specifying and checking file system crash-consistency models. In: Proceedings of ASPLOS, pp. 83\u201398. ACM (2016)","DOI":"10.1145\/2872362.2872406"},{"issue":"4","key":"25_CR4","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/3051092","volume":"60","author":"T Chajed","year":"2017","unstructured":"Chajed, T., Chen, H., Chlipala, A., Kaashoek, M.F., Zeldovich, N., Ziegler, D.: Certifying a file system using crash hoare logic: correctness in the presence of crashes. Commun. ACM 60(4), 75\u201384 (2017)","journal-title":"Commun. ACM"},{"key":"25_CR5","unstructured":"Chen, H.: Certifying a crash-safe file system. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, United States (2016)"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Chen, H., Ziegler, D., Chlipala, A., Zeldovich, N., Kaashoek, M.F.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of the Symposium on Operating Systems Principles (SOSP). ACM (2015)","DOI":"10.1145\/2815400.2815402"},{"key":"25_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W-P Roever de","year":"1998","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)"},{"issue":"6","key":"25_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV-overview and verifythis competition. Softw. Tools Technol. Transf. (STTT) 17(6), 677\u2013694 (2015)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-319-29613-5_5","volume-title":"Verified Software: Theories, Tools, and Experiments","author":"G Ernst","year":"2016","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Inside a verified flash file system: transactions and garbage collection. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 73\u201393. Springer, Cham (2016). doi:\n10.1007\/978-3-319-29613-5_5"},{"key":"25_CR10","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2016.04.009","volume":"131","author":"G Ernst","year":"2016","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. (SCP) 131, 3\u201321 (2016)","journal-title":"Sci. Comput. Program. (SCP)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-54108-7_13","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G Ernst","year":"2014","unstructured":"Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., Reif, W.: Verification of a virtual filesystem switch. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 242\u2013261. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54108-7_13"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"J He","year":"1986","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined resume. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187\u2013196. Springer, Heidelberg (1986). doi:\n10.1007\/3-540-16442-1_14"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Koskinen, E., Yang, J.: Reducing crash recoverability to reachability. In: Proceedings of Principles of Programming Languages (POPL), pp. 97\u2013108. ACM (2016)","DOI":"10.1145\/2837614.2837648"},{"issue":"12","key":"25_CR14","first-page":"602","volume":"3","author":"MI Lali","year":"2013","unstructured":"Lali, M.I.: File system formalization: revisited. Int. J. Adv. Comput. Sci. 3(12), 602\u2013606 (2013)","journal-title":"Int. J. Adv. Comput. Sci."},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-06410-9_31","volume-title":"FM 2014: Formal Methods","author":"O Mari\u0107","year":"2014","unstructured":"Mari\u0107, O., Sprenger, C.: Verification of a transactional memory manager under hardware failures and restarts. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 449\u2013464. Springer, Cham (2014). doi:\n10.1007\/978-3-319-06410-9_31"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-319-26529-2_10","volume-title":"Programming Languages and Systems","author":"G Ntzik","year":"2015","unstructured":"Ntzik, G., da Rocha Pinto, P., Gardner, P.: Fault-tolerant resource reasoning. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 169\u2013188. Springer, Cham (2015). doi:\n10.1007\/978-3-319-26529-2_10"},{"issue":"1","key":"25_CR17","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/146941.146943","volume":"10","author":"M Rosenblum","year":"1992","unstructured":"Rosenblum, M., Ousterhout, J.K.: The design and implementation of a log-structured file system. ACM Trans. Comput. Syst. (TOCS) 10(1), 26\u201352 (1992)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-662-43652-3_2","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Ernst, G., Pf\u00e4hler, J., Haneberg, D., Reif, W.: Development of a verified flash file system. ABZ 2014. LNCS, vol. 8477, pp. 9\u201324. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-662-43652-3_2"},{"key":"25_CR19","unstructured":"Sigurbjarnarson, H., Bornholt, J., Torlak, E., Wang, X.: Push-button verification of file systems via crash refinement. In: Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association (2016)"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Tseng, H-W., Grupp, L., Swanson, S.: Understanding the impact of power loss on flash memory. In: Proceedings of the Design Automation Conference (DAC), pp. 35\u201340. ACM (2011)","DOI":"10.1145\/2024724.2024733"},{"key":"25_CR21","unstructured":"Tweedie, S.C.: Journaling the Linux ext2fs filesystem. In: The Fourth Annual Linux Expo (1998)"},{"key":"25_CR22","volume-title":"Using Z: Specification, Proof and Refinement","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall, Upper Saddle River (1996)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:44:47Z","timestamp":1503747887000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}