{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:20:20Z","timestamp":1759990820604},"reference-count":32,"publisher":"Elsevier BV","issue":"4","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":1663,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1016\/j.scico.2008.09.014","type":"journal-article","created":{"date-parts":[[2008,10,5]],"date-time":"2008-10-05T08:06:25Z","timestamp":1223193985000},"page":"219-237","source":"Crossref","is-referenced-by-count":21,"title":["Mechanising a formal model of flash memory"],"prefix":"10.1016","volume":"74","author":[{"given":"Andrew","family":"Butterfield","sequence":"first","affiliation":[]},{"given":"Leo","family":"Freitas","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2008.09.014_b1","unstructured":"Galloway Andy, R.S. Jan Tobias M\u00fchlberg, G. L\u00fcttgen, Model-checking part of a Linux file system, Technical Report YCS-2007-423, Department of Computer Science, University of York, 2007. URL: http:\/\/www.cs.york.ac.uk\/ftpdir\/reports\/YCS-2007-423.pdf"},{"issue":"5","key":"10.1016\/j.scico.2008.09.014_b2","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1109\/5.220908","article-title":"Reliability issues of flash memory cells (invited paper)","volume":"81","author":"Aritome","year":"1993","journal-title":"Proceedings of the IEEE"},{"key":"10.1016\/j.scico.2008.09.014_b3","series-title":"ICFEM","first-page":"373","article-title":"Verifying a file system implementation","volume":"vol. 3308","author":"Arkoudas","year":"2004"},{"key":"10.1016\/j.scico.2008.09.014_b4","series-title":"12th IEEE International Conference on Engineering Complex Computer Systems, 2007","first-page":"251","article-title":"Formalising flash memory: First steps","author":"Butterfield","year":"2007"},{"key":"10.1016\/j.scico.2008.09.014_b5","unstructured":"L. Freitas, Crg-12. Tech. rep., University of York, 2007. www.cs.york.ac.uk\/circus\/mc\/reports"},{"key":"10.1016\/j.scico.2008.09.014_b6","unstructured":"L. Freitas, A. Butterfield, J. Woodcock, ONFi specification in Z\/Eves flash memory hardware specification, Tech. Rep., High Integrity Systems Engineering (HISE) Group, University of York, 2007. URL: www.cs.york.ac.uk\/circus\/mc\/reports\/CRG-12.pdf"},{"issue":"6","key":"10.1016\/j.scico.2008.09.014_b7","doi-asserted-by":"crossref","first-page":"81","DOI":"10.5381\/jot.2004.3.6.a4","article-title":"Checking concise specifications for multithreaded software","volume":"3","author":"Freund","year":"2004","journal-title":"Journal of Object Technology"},{"key":"10.1016\/j.scico.2008.09.014_b8","article-title":"Algorithms and data structures for flash memories","volume":"37","author":"Gal","year":"2005","journal-title":"CSURV: Computing Surveys"},{"key":"10.1016\/j.scico.2008.09.014_b9","series-title":"Algebraic Methodology and Software Technology","first-page":"475","article-title":"Specification of the Unix file system: A comparative case study","author":"Heisel","year":"1995"},{"issue":"1","key":"10.1016\/j.scico.2008.09.014_b10","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/602382.602403","article-title":"The verifying compiler: A grand challenge for computing research","volume":"50","author":"Hoare","year":"2003","journal-title":"Journal of the ACM"},{"key":"10.1016\/j.scico.2008.09.014_b11","unstructured":"Hynix Semiconductor, et al. Open NAND flash interface specification, Tech. Rep. Revision 1.0, ONFI, 28th December 2006. www.onfi.org"},{"key":"10.1016\/j.scico.2008.09.014_b12","unstructured":"Intel, Intel\u00ae flash file system core reference guide, version 1. Manual 304436\u2013001, Intel Corporation, October 2004. URL: sunsite.rediris.es\/pub\/mirror\/intel\/flcomp\/manuals\/30443601.pdf"},{"key":"10.1016\/j.scico.2008.09.014_b13","unstructured":"R. Joshi, G.J. Holzmann, A mini challenge: Build a verifiable filesystem, in: Proc. Verified Software: Theories, Tools, Experiments, VSTTE, Z\u00fcrich, 2005"},{"key":"10.1016\/j.scico.2008.09.014_b14","series-title":"Proceedings of the 2006 International Conference on Compilers, Architecture and Synthesis for Embedded Systems","first-page":"103","article-title":"Flashcache: A NAND flash memory file cache for low power web servers","author":"Kgil","year":"2006"},{"key":"10.1016\/j.scico.2008.09.014_b15","series-title":"COMPSAC","first-page":"284","article-title":"A new flash memory management for flash storage system","author":"Kim","year":"1999"},{"key":"10.1016\/j.scico.2008.09.014_b16","series-title":"ICST","first-page":"475","article-title":"Pre-testing flash device driver through model checking techniques","author":"Kim","year":"2008"},{"issue":"7","key":"10.1016\/j.scico.2008.09.014_b17","doi-asserted-by":"crossref","first-page":"906","DOI":"10.1109\/TC.2006.96","article-title":"An efficient NAND flash file system for flash memory storage","volume":"55","author":"Lim","year":"2006","journal-title":"IEEE Transactions on Computers"},{"key":"10.1016\/j.scico.2008.09.014_b18","unstructured":"C. Manning, Introducing YAFFS, the first NAND-specific flash file system, LinuxDevices.com, Sep 2002. URL: http:\/\/www.linuxdevices.com\/articles\/AT9680239525.html"},{"key":"10.1016\/j.scico.2008.09.014_b19","first-page":"451","article-title":"Flash memory file caching for mobile computers","volume":"vol. 1","author":"Marsh","year":"1994"},{"key":"10.1016\/j.scico.2008.09.014_b20","first-page":"80","article-title":"The Unix filing system: A MooZ specification","author":"Meira","year":"1994"},{"key":"10.1016\/j.scico.2008.09.014_b21","unstructured":"I. Meisels, M. Saaltink, The Z\/EVES reference manual (for version 1.5), 1997. URL: http:\/\/citeseer.ist.psu.edu\/351588.html"},{"key":"10.1016\/j.scico.2008.09.014_b22","series-title":"Specification Case Studies","first-page":"91","article-title":"Specification of the Unix filing system","author":"Morgan","year":"1987"},{"key":"10.1016\/j.scico.2008.09.014_b23","unstructured":"P.R.H. Place, POSIX 1003.21 \u2014 Real time distributed systems communication, Tech. Rep., Software Engineering Institute, Carnegie Mellon University, August 1995. URL: ftp:\/\/ftp.sei.cmu.edu\/pub\/posix\/formal\/full_spec_2.ps.Z"},{"key":"10.1016\/j.scico.2008.09.014_b24","unstructured":"M. Saaltink, The Z\/EVES 2.0 user\u2019s guide, Jun. 30 2004. URL: http:\/\/citeseer.ist.psu.edu\/676306.html"},{"key":"10.1016\/j.scico.2008.09.014_b25","series-title":"ACSAC","first-page":"13","article-title":"Model checking an entire Linux distribution for security violations","author":"Schwarz","year":"2005"},{"issue":"12","key":"10.1016\/j.scico.2008.09.014_b26","doi-asserted-by":"crossref","first-page":"1980","DOI":"10.1016\/j.microrel.2006.01.003","article-title":"Technologies and reliability of modern embedded flash cells","volume":"46","author":"Sikora","year":"2006","journal-title":"Microelectronics Reliability"},{"key":"10.1016\/j.scico.2008.09.014_b27","series-title":"The Z Notation: A Reference Manual","author":"Spivey","year":"1992"},{"issue":"10","key":"10.1016\/j.scico.2008.09.014_b28","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/MC.2006.340","article-title":"First steps in the verified software grand challenge","volume":"39","author":"Woodcock","year":"2006","journal-title":"IEEE Computer"},{"key":"10.1016\/j.scico.2008.09.014_b29","author":"Woodcock","year":"1996"},{"key":"10.1016\/j.scico.2008.09.014_b30","series-title":"ICTAC","first-page":"15","article-title":"Z\/Eves and the Mondex electronic purse","volume":"vol. 4281","author":"Woodcock","year":"2006"},{"key":"10.1016\/j.scico.2008.09.014_b31","unstructured":"D. Woodhouse, JFFS: The journalling flash file system, in: Ottawa Linux Symposium 2001, Oct 2001. URL: http:\/\/sourceware.org\/jffs2\/jffs2.pdf"},{"issue":"4","key":"10.1016\/j.scico.2008.09.014_b32","doi-asserted-by":"crossref","first-page":"393","DOI":"10.1145\/1189256.1189259","article-title":"Using model checking to find serious file system errors","volume":"24","author":"Yang","year":"2006","journal-title":"ACM Transactions on Computer Systems"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642308001238?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642308001238?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,25]],"date-time":"2018-12-25T08:50:03Z","timestamp":1545727803000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642308001238"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["S0167642308001238"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2008.09.014","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2009,2]]}}}