{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:57:58Z","timestamp":1725541078334},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_12","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"226-245","source":"Crossref","is-referenced-by-count":2,"title":["RAFFS: Model Checking a Robust Abstract Flash File Store"],"prefix":"10.1007","author":[{"given":"Paul","family":"Taverne","sequence":"first","affiliation":[]},{"given":"C. (Kees)","family":"Pronk","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"ABZ conference: case study details, http:\/\/www.cs.york.ac.uk\/circus\/mc\/abz\/"},{"key":"12_CR2","unstructured":"ABZ conference (October 2008), http:\/\/www.abz2008.org\/"},{"key":"12_CR3","unstructured":"Arkoudas, K.: Athena, http:\/\/www.cag.csail.mit.edu\/~kostas\/dpls\/athena\/"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.: On verifying a file system implementation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 373\u2013390. Springer, Heidelberg (2004)"},{"issue":"2","key":"12_CR5","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s00165-005-0079-4","volume":"18","author":"J.C. Bicarregui","year":"2006","unstructured":"Bicarregui, J.C., Hoare, C.A.R., Woodcock, J.C.P.: The verified software repository: a step towards the verifying compiler. Formal Aspects of Computing\u00a018(2), 143\u2013151 (2006)","journal-title":"Formal Aspects of Computing"},{"key":"12_CR6","unstructured":"Butler, M.: Some filestore developments with Event-B and RODIN. In: Workshop at ICFEM (2007)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Butterfield, A., Woodcock, J.: Formalising flash memory: First steps. In: ICECCS, pp. 251\u2013260 (2007)","DOI":"10.1109\/ICECCS.2007.23"},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1145\/1278480.1278533","volume-title":"DAC 2007: Proceedings of the 44th annual conference on Design automation","author":"Y.-H. Chang","year":"2007","unstructured":"Chang, Y.-H., Hsieh, J.-W., Kuo, T.-W.: Endurance enhancement of flash-memory storage systems: an efficient static wear leveling design. In: DAC 2007: Proceedings of the 44th annual conference on Design automation, pp. 212\u2013217. ACM, New York (2007)"},{"key":"12_CR9","first-page":"1","volume-title":"structured programming","author":"E.W. Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: Notes on structured programming. In: Dahl, O.J., Dijkstra, E.W., Hoare, C.A.R. (eds.) structured programming, Ch.\u00a01, pp. 1\u201382. Academic Press, London (1972)"},{"key":"12_CR10","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. Newcastle University, CS-TR-1099 (May 2008)"},{"key":"12_CR11","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: ICECCS, pp. 3\u201314 (2007)","DOI":"10.1109\/ICECCS.2007.36"},{"key":"12_CR12","volume-title":"13th Int\u2019l Conference on Engineering Complex Computer Systems (ICECCS 2008)","author":"L. Freitas","year":"2008","unstructured":"Freitas, L., Woodcock, J., Butterfield, A.: POSIX and the verification grand challenge: a roadmap. In: 13th Int\u2019l Conference on Engineering Complex Computer Systems (ICECCS 2008). IEEE, Los Alamitos (2008)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-93900-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Galloway","year":"2009","unstructured":"Galloway, A., L\u00fcttgen, G., M\u00fchlberg, J.T., Siminiceanu, R.I.: Model-checking the Linux virtual file system. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 74\u201388. Springer, Heidelberg (2009)"},{"key":"12_CR14","unstructured":"Grand Challenge 6, http:\/\/vsr.sourceforge.net\/gc6index.htm"},{"key":"12_CR15","first-page":"621","volume-title":"ICSE 2007: Proceedings of the 29th Int\u2019l conference on Software Engineering","author":"A. Groce","year":"2007","unstructured":"Groce, A., Holzmann, G., Joshi, R.: Randomized differential testing as a prelude to formal verification. In: ICSE 2007: Proceedings of the 29th Int\u2019l conference on Software Engineering, pp. 621\u2013631. IEEE Computer Society, Los Alamitos (2007)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., et al.: Temporal safety-proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"12_CR17","unstructured":"Hoare, T., Misra, J.: Verified software: theories, tools, experiments (July 2005), http:\/\/vstte.ethz.ch"},{"key":"12_CR18","unstructured":"Holzmann, G.J.: Promela language reference, http:\/\/www.spinroot.com\/spin\/Man\/promela.html"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Bo\u0161na\u010dki, D.: The design of a multi-core extension of the Spin model checker. IEEE Transactions on Software Engineering\u00a033(10) (October 2007)","DOI":"10.1109\/TSE.2007.70724"},{"key":"12_CR20","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1002\/spe.4380180203","volume":"18","author":"G.J. Holzmann","year":"1988","unstructured":"Holzmann, G.J.: An improved reachability analysis technique. Software Practice and Experience\u00a018, 137\u2013161 (1988)","journal-title":"Software Practice and Experience"},{"key":"12_CR21","volume-title":"Proc. Third SPIN Workshop","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: State compression in SPIN. In: Proc. Third SPIN Workshop, Twente University, The Netherlands (1997)"},{"key":"12_CR22","volume-title":"The SPIN Model Checker : Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-540-69850-0_4","volume-title":"25 Years of Model Checking","author":"G.J. Holzmann","year":"2006","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: New challenges in model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 65\u201376. Springer, Heidelberg (2006)"},{"issue":"3","key":"12_CR24","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/s100090050034","volume":"2","author":"G.J. Holzmann","year":"1999","unstructured":"Holzmann, G.J., Puri, A.: A minimized automaton representation of reachable states. Software Tools for Technology Transfer\u00a02(3), 270\u2013278 (1999)","journal-title":"Software Tools for Technology Transfer"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"588","DOI":"10.1007\/3-540-54834-3_34","volume-title":"VDM \u201991","author":"I. Houston","year":"1991","unstructured":"Houston, I., King, S.: CICS project report: Experiences and results from the use of Z. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol.\u00a0551, pp. 588\u2013596. Springer, Heidelberg (1991)"},{"key":"12_CR26","unstructured":"ICFEM Flash File System Workshop. Modelling Flash Memory (November 2007)"},{"key":"12_CR27","unstructured":"Intel Corporation. Intel Flash File System Core Reference Guide, version 1 edition (October 2004)"},{"key":"12_CR28","volume-title":"Software Abstractions","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions. The MIT-Press, Cambridge (2006)"},{"issue":"4","key":"12_CR29","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C. Jones","year":"2006","unstructured":"Jones, C., O\u2019Hearn, P., Woodcock, J.: Verified software: A grand challenge. IEEE Computer: Software Technologies\u00a039(4), 93\u201395 (2006)","journal-title":"IEEE Computer: Software Technologies"},{"issue":"2","key":"12_CR30","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/s00165-006-0022-3","volume":"19","author":"R. Joshi","year":"2007","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Formal Aspects of Computing\u00a019(2), 269\u2013272 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"12_CR31","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)"},{"key":"12_CR32","doi-asserted-by":"publisher","first-page":"1621","DOI":"10.1145\/1529282.1529648","volume-title":"SAC 2009: Proceedings of the, ACM symposium on Applied Computing","author":"Z. Liu","year":"2009","unstructured":"Liu, Z., Yue, L., Wei, P., Jin, P., Xiang, X.: An adaptive block-set based management for large-scale flash memory. In: SAC 2009: Proceedings of the, ACM symposium on Applied Computing, pp. 1621\u20131625. ACM, New York (2009)"},{"issue":"2","key":"12_CR33","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TSE.1984.5010215","volume":"10","author":"C. Morgan","year":"1984","unstructured":"Morgan, C., Sufrin, B.: Specification of the UNIX filing system. IEEE Trans. Software Eng.\u00a010(2), 128\u2013142 (1984)","journal-title":"IEEE Trans. Software Eng."},{"key":"12_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-70952-7_14","volume-title":"Formal Methods: Applications and Technology","author":"J.T. M\u00fchlberg","year":"2007","unstructured":"M\u00fchlberg, J.T., L\u00fcttgen, G.: Blasting Linux code. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 211\u2013226. Springer, Heidelberg (2007)"},{"key":"12_CR35","unstructured":"Part 1: Base\u00a0definitions POSIX. ISO\/IEC 9945-1:2003"},{"key":"12_CR36","unstructured":"Part 2: System\u00a0Interfaces POSIX. ISO\/IEC 9945-2:2003"},{"key":"12_CR37","unstructured":"Ruys, T.C.: Towards Effective Model Checking. PhD thesis, University of Twente, Enschede (March 2001)"},{"key":"12_CR38","volume-title":"The Z notation: a reference manual","author":"J.M. Spivey","year":"1989","unstructured":"Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall, Inc., Upper Saddle River (1989)"},{"key":"12_CR39","unstructured":"Taverne, P.: Raffs: Model checking a robust abstract flash file store. Master\u2019s thesis, Delft University of Technology (2009), http:\/\/repository.tudelft.nl\/view\/ir\/uuid%3A2b4a1434-8169-481d-9824-fe79e9c4874c"},{"key":"12_CR40","unstructured":"Verified software repository, http:\/\/vsr.sourceforge.net"},{"key":"12_CR41","unstructured":"Verified software: Theories, tools, experiments (October 2005), http:\/\/vstte.inf.ethz.ch\/"},{"issue":"4","key":"12_CR42","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1145\/1189256.1189259","volume":"24","author":"J. Yang","year":"2006","unstructured":"Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. ACM Trans. Comput. Syst.\u00a024(4), 393\u2013423 (2006)","journal-title":"ACM Trans. Comput. Syst."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:54:52Z","timestamp":1606186492000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}