Output details
11 - Computer Science and Informatics
University of York
Article title
Mechanising a formal model of flash memory
Type
D - Journal article
Title of journal
Science of Computer Programming
Article number
-
Volume number
74
Issue number
4
First page of article
219
ISSN of journal
0167-6423
Year of publication
2009
Number of additional authors
2
Additional information
<07>Originality: Joshi and Holzmann established a flash filestore for space-flight applications as a challenge problem for software verification. Our work pushes the problem boundary into the algorithms and data structures used in the implementation of flash memory. Rigour: The mechanisation is conducted in the Z/Eves theorem prover and the work is repeatable using models and proofs scripts publicly available. Significance: This paper has inspired many people to work at this level. The work fed back into the Open NAND Flash Interface industry workgroup, composed of more than 100 companies, identifying issues of incompleteness and ambiguity in the current standard.
Interdisciplinary
-
Cross-referral requested
-
Research group
A - High Integrity Systems Engineering
Citation count
12
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
