{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,29]],"date-time":"2025-10-29T02:52:24Z","timestamp":1761706344142,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296128"},{"type":"electronic","value":"9783319296135"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-29613-5_5","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"73-93","source":"Crossref","is-referenced-by-count":11,"title":["Inside a Verified Flash File System: Transactions and Garbage Collection"],"prefix":"10.1007","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[]},{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","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)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from Microkernel verification - specification is the new bottleneck. In: SSV, pp. 18\u201332 (2012)","DOI":"10.4204\/EPTCS.102.4"},{"issue":"1\u20132","key":"5_CR3","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s00165-003-0012-7","volume":"15","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM refinement method. Form. Asp. Comput. 15(1\u20132), 237\u2013257 (2003)","journal-title":"Form. Asp. Comput."},{"key":"5_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines \u2013 A Method for High-Level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines \u2013 A Method for High-Level System Design and Analysis. Springer, Berlin (2003)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Butterfield, A., Woodcock, J.: Formalising flash memory: first steps. In: IEEE International Conference on Engineering of Complex Computer Systems, pp. 251\u2013260 (2007)","DOI":"10.1109\/ICECCS.2007.23"},{"key":"5_CR6","unstructured":"Chen, H., Ziegler, D., Chlipala, A., Kaashoek, M.F., Kohler, E., Zeldovich, N.: Specifying crash safety for storage systems. In: 15th Workshop on Hot Topics in Operating Systems (HotOS XV). USENIX Association (2015)"},{"key":"5_CR7","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 SOSP. ACM (2015)","DOI":"10.1145\/2815400.2815402"},{"key":"5_CR8","unstructured":"Damchoom, K.: An incremental refinement approach to a development of a flash-based file system in Event-B, Ph.D. thesis, University of Southampton (2010)"},{"key":"5_CR9","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G.: Web presentation of the Flash Filesystem (2015). \n                    https:\/\/swt.informatik.uni-augsburg.de\/swt\/projects\/flash.html"},{"issue":"6","key":"5_CR10","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"Gidon Ernst","year":"2014","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":"International Journal on Software Tools for Technology Transfer"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Modular, crash-safe refinement for ASMs with submachines. Science of Computer Programming, ABZ special issue, 2015 (submitted) (2014)","DOI":"10.1016\/j.scico.2016.04.009"},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"33","DOI":"10.4204\/EPTCS.102.5","volume":"102","author":"Gidon Ernst","year":"2012","unstructured":"Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., Reif, W.: A formal model of a virtual filesystem switch. In: Proceedings of Software and Systems Modeling (SSV), EPTCS, pp. 33\u201345 (2012)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"5_CR13","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)"},{"key":"5_CR14","unstructured":"Ferreira, M.A., Silva, S.S., Oliveira, J.N.: Verifying intel Flash File System core specification. In: Modelling and Analysis in VDM: Proceedings of the Fourth VDM\/Overture Workshop, pp. 54\u201371, Technical report CS-TR-1099 (2008)"},{"issue":"4","key":"5_CR15","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.scico.2008.08.001","volume":"74","author":"L Freitas","year":"2009","unstructured":"Freitas, L., Woodcock, J., Fu, Z.: POSIX file store in Z\/Eves: an experiment in the verified software repository. Sci. Comput. Program. 74(4), 238\u2013257 (2009)","journal-title":"Sci. Comput. Program."},{"key":"5_CR16","unstructured":"Gleixner, T., Haverkamp, F., Bityutskiy, A.: UBI - Unsorted Block Images (2006). \n                    http:\/\/www.linux-mtd.infradead.org\/doc\/ubidesign\/ubidesign.pdf"},{"issue":"1","key":"5_CR17","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s00165-010-0171-2","volume":"24","author":"WH Hesselink","year":"2012","unstructured":"Hesselink, W.H., Lali, M.I.: Formalizing a hierarchical file system. Form. Asp. Comput. 24(1), 27\u201344 (2012)","journal-title":"Form. Asp. Comput."},{"key":"5_CR18","unstructured":"Hunter, A.: A brief introduction to the design of UBIFS (2008). \n                    http:\/\/www.linux-mtd.infradead.org\/doc\/ubifs_whitepaper.pdf"},{"issue":"2","key":"5_CR19","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/s00165-006-0022-3","volume":"19","author":"Rajeev Joshi","year":"2007","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Form. Asp. Comput. 19(2), 269\u2013272 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-87603-8_23","volume-title":"Abstract State Machines, B and Z","author":"E Kang","year":"2008","unstructured":"Kang, E., Jackson, D.: Formal Modeling and Analysis of a Flash Filesystem in Alloy. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 294\u2013308. Springer, Heidelberg (2008)"},{"key":"5_CR21","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, Heidelberg (2014)"},{"key":"5_CR22","first-page":"91","volume-title":"Specification Case Studies","author":"C Morgan","year":"1987","unstructured":"Morgan, C., Sufrin, B.: Specification of the UNIX filing system. Specification Case Studies, pp. 91\u2013140. Prentice Hall Ltd., Hertfordshire (1987)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-03077-7_15","volume-title":"Hardware and Software: Verification and Testing","author":"J Pf\u00e4hler","year":"2013","unstructured":"Pf\u00e4hler, J., Ernst, G., Schellhorn, G., Haneberg, D., Reif, W.: Formal specification of an erase block management layer for flash memory. In: Legay, A., Bertacco, V. (eds.) HVC 2013. LNCS, vol. 8244, pp. 214\u2013229. Springer, Heidelberg (2013)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Ridge, T., Sheets, D., Tuerk, T., Giugliano, A., Madhavapeddy, A., Sewell, P.: SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. In: Proceedings of SOSP. ACM (2015)","DOI":"10.1145\/2815400.2815411"},{"issue":"9","key":"5_CR25","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1016\/j.scico.2009.10.004","volume":"76","author":"G Schellhorn","year":"2009","unstructured":"Schellhorn, G.: Completeness of fair ASM refinement. Sci. Comput. Program. 76(9), 756\u2013773 (2009). Elsevier","journal-title":"Sci. Comput. Program."},{"key":"5_CR26","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. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 9\u201324. Springer, Heidelberg (2014)"},{"key":"5_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10472-014-9417-7","volume":"71","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Pf\u00e4hler, J., Reif, W.: RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. (AMAI) 71, 1\u201344 (2014)","journal-title":"Ann. Math. Artif. Intell. (AMAI)"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-05089-3_13","volume-title":"FM 2009: Formal Methods","author":"A Schierl","year":"2009","unstructured":"Schierl, A., Schellhorn, G., Haneberg, D., Reif, W.: Abstract specification of the UBIFS file system for flash memory. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 190\u2013206. Springer, Heidelberg (2009)"},{"key":"5_CR29","unstructured":"The Open Group: The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2008 Edition. \n                    http:\/\/www.unix.org\/version3\/online.html\n                    \n                   (login required)"},{"key":"5_CR30","unstructured":"UBI - Out-of-Band Data. \n                    http:\/\/www.linux-mtd.infradead.org\/faq\/ubi.html"},{"key":"5_CR31","series-title":"Prentice Hall International Series in Computer Science","volume-title":"Using Z: Specification. Proof and Refinement","author":"JCP Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification. Proof and Refinement. Prentice Hall International Series in Computer Science. Prentice Hall, New York (1996)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T07:51:14Z","timestamp":1559375474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}