{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:29Z","timestamp":1763468189296},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662436516"},{"type":"electronic","value":"9783662436523"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43652-3_2","type":"book-chapter","created":{"date-parts":[[2014,5,28]],"date-time":"2014-05-28T22:22:12Z","timestamp":1401315732000},"page":"9-24","source":"Crossref","is-referenced-by-count":24,"title":["Development of a Verified Flash File System"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[]},{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Haneberg","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_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.\u00a03308, pp. 373\u2013390. Springer, Heidelberg (2004)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-45821-2_4","volume-title":"Generative Programming and Component Engineering","author":"G. Back","year":"2002","unstructured":"Back, G.: DataScript - A Specification and Scripting Language for Binary Data. In: Batory, D., Blum, A., Taha, W. (eds.) GPCE 2002. LNCS, vol.\u00a02487, pp. 66\u201377. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons Learned From Microkernel Verification \u2013 Specification is the New Bottleneck. In: SSV, pp. 18\u201332 (2012)","key":"2_CR3","DOI":"10.4204\/EPTCS.102.4"},{"issue":"1-2","key":"2_CR4","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. Formal Aspects of Computing\u00a015(1-2), 237\u2013257 (2003)","journal-title":"Formal Aspects of Computing"},{"doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines \u2014 A Method for High-Level System Design and Analysis. Springer (2003)","key":"2_CR5","DOI":"10.1007\/978-3-642-18216-7"},{"doi-asserted-by":"crossref","unstructured":"Butterfield, A., Woodcock, J.: Formalising Flash Memory: First Steps. In: IEEE Int. Conf. on Engineering of Complex Computer Systems, pp. 251\u2013260 (2007)","key":"2_CR6","DOI":"10.1109\/ICECCS.2007.23"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"unstructured":"http:\/\/www.garz-fricke.com\/cupid-core_de.html","key":"2_CR8"},{"unstructured":"Damchoom, K.: An incremental refinement approach to a development of a flash-based file system in Event-B (October 2010)","key":"2_CR9"},{"unstructured":"Samsung Electronics. Page program addressing for MLC NAND application note (2009), http:\/\/www.samsung.com","key":"2_CR10"},{"unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G.: Web presentation of the Flash Filesystem (2014), https:\/\/swt.informatik.uni-augsburg.de\/swt\/projects\/flash.html","key":"2_CR11"},{"doi-asserted-by":"crossref","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - Overview and VerifyThis Competition. Software Tools for Technology Transfer (to appear, 2014)","key":"2_CR12","DOI":"10.1007\/s10009-014-0308-3"},{"key":"2_CR13","series-title":"LNCS","first-page":"188","volume-title":"ABZ 2014","author":"G. Ernst","year":"2014","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Modular Refinement for Submachines of ASMs. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol.\u00a08477, pp. 188\u2013203. Springer, Heidelberg (2014)"},{"doi-asserted-by":"crossref","unstructured":"Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., Reif, W.: A Formal Model of a Virtual Filesystem Switch. In: Proc. of Software and Systems Modeling (SSV), pp. 33\u201345 (2012)","key":"2_CR14","DOI":"10.4204\/EPTCS.102.5"},{"key":"2_CR15","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.\u00a08164, pp. 242\u2013261. Springer, Heidelberg (2014)"},{"unstructured":"Intel Corporation, et al.: Open NAND Flash Interface Specification (June 2013), http:\/\/www.onfi.org","key":"2_CR16"},{"unstructured":"Ferreira, M.A., Silva, S.S., Oliveira, J.N.: Verifying Intel flash file system core specification. In: Modelling and Analysis in VDM: Proc. of the Fourth VDM\/Overture Workshop, School of Computing Science, Newcastle University, Technical Report CS-TR-1099, pp. 54\u201371 (2008)","key":"2_CR17"},{"doi-asserted-by":"crossref","unstructured":"Freitas, L., Woodcock, J., Butterfield, A.: POSIX and the Verification Grand Challenge: A Roadmap. In: ICECCS 2008: Proc. of the 13th IEEE Int. Conf. on Engineering of Complex Computer Systems (2008)","key":"2_CR18","DOI":"10.1109\/ICECCS.2008.35"},{"issue":"4","key":"2_CR19","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. of Comp. Programming\u00a074(4), 238\u2013257 (2009)","journal-title":"Sci. of Comp. Programming"},{"unstructured":"Gleixner, T., Haverkamp, F., Bityutskiy, A.: UBI - Unsorted Block Images (2006), http:\/\/www.linux-mtd.infradead.org\/doc\/ubidesign\/ubidesign.pdf","key":"2_CR20"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/s00165-010-0171-2","volume":"24","author":"W.H. Hesselink","year":"2012","unstructured":"Hesselink, W.H., Lali, M.I.: Formalizing a hierarchical file system. Formal Aspects of Computing\u00a024(1), 27\u201344 (2012)","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. Journal of the ACM\u00a050(1), 63\u201369 (2003)","journal-title":"Journal of the ACM"},{"unstructured":"Hunter, A.: A brief introduction to the design of UBIFS (2008), http:\/\/www.linux-mtd.infradead.org\/doc\/ubifs_whitepaper.pdf","key":"2_CR23"},{"doi-asserted-by":"crossref","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Formal Aspects of Computing\u00a019(2) (June 2007)","key":"2_CR24","DOI":"10.1007\/s00165-006-0022-3"},{"key":"2_CR25","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.\u00a05238, pp. 294\u2013308. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"2_CR26","first-page":"129","volume":"3","author":"E. Kang","year":"2009","unstructured":"Kang, E., Jackson, D.: Designing and Analyzing a Flash File System with Alloy. Int. J. Software and Informatics\u00a03(2-3), 129\u2013148 (2009)","journal-title":"Int. J. Software and Informatics"},{"issue":"4","key":"2_CR27","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/347057.347563","volume":"30","author":"P.J. McCann","year":"2000","unstructured":"McCann, P.J., Chandra, S.: Packet Types: Abstract Specification of Network Protocol Messages. SIGCOMM Comp. Comm. Rev.\u00a030(4), 321\u2013333 (2000)","journal-title":"SIGCOMM Comp. Comm. Rev."},{"key":"2_CR28","first-page":"91","volume-title":"Specification Case Studies","author":"C. Morgan","year":"1987","unstructured":"Morgan, C., Sufrin, B.: Specification of the unix filing system. In: Specification Case Studies, pp. 91\u2013140. Prentice Hall Ltd., Hertfordshire (1987)"},{"unstructured":"Memory Technology Device (MTD) and Unsorted Block Images (UBI) Subsystem of Linux, http:\/\/www.linux-mtd.infradead.org\/index.html","key":"2_CR29"},{"key":"2_CR30","volume-title":"Programming in Scala: A Comprehensive Step-by-step Guide","author":"M. Odersky","year":"2008","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A Comprehensive Step-by-step Guide, 1st edn. Artima Incorporation, USA (2008)","edition":"1"},{"issue":"3","key":"2_CR31","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1109\/TSE.2012.15","volume":"39","author":"J.N. Oliveira","year":"2013","unstructured":"Oliveira, J.N., Ferreira, M.A.: Alloy Meets the Algebra of Programming: A Case Study. IEEE Transactions on Software Engineering\u00a039(3), 305\u2013326 (2013)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR32","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: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol.\u00a08244, pp. 214\u2013229. Springer, Heidelberg (2013)"},{"unstructured":"Pf\u00e4hler, J., Ernst, G., Schellhorn, G., Haneberg, D., Reif, W.: Crash-Safe Refinement for a Verified Flash File System. Technical report, University of Augsburg (2014)","key":"2_CR33"},{"doi-asserted-by":"crossref","unstructured":"Reeves, G., Neilson, T.: The Mars Rover Spirit FLASH anomaly. In: Aerospace Conference, pp. 4186\u20134199. IEEE Computer Society (2005)","key":"2_CR34","DOI":"10.1109\/AERO.2005.1559723"},{"key":"2_CR35","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"W. Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, vol.\u00a0II, pp. 13\u201339. Kluwer, Dordrecht (1998)"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of LICS, pp. 55\u201374. IEEE Computer Society (2002)","key":"2_CR36","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"9","key":"2_CR37","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Transactions on Software Engineering\u00a024(9), 709\u2013720 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"doi-asserted-by":"crossref","unstructured":"Schellhorn, G.: Completeness of Fair ASM Refinement. Science of Computer Programming\u00a076(9) (2009)","key":"2_CR38","DOI":"10.1016\/j.scico.2009.10.004"},{"key":"2_CR39","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.\u00a05850, pp. 190\u2013206. Springer, Heidelberg (2009)"},{"unstructured":"Szeredi, M.: File system in user space, http:\/\/fuse.sourceforge.net","key":"2_CR40"},{"unstructured":"The Open Group. The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2008 Edition (2008), http:\/\/www.unix.org\/version3\/online.html (login required)","key":"2_CR41"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43652-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,10]],"date-time":"2019-08-10T23:24:21Z","timestamp":1565479461000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43652-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436516","9783662436523"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43652-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}