@inproceedings(ArkoudasKuncak-ICFEM04, author = "K. Arkoudas and K. Zee and V. Kuncak and M. C. Rinard", year = "2004", title = "On Verifying a File System Implementation", booktitle = "ICFEM", pages = "373--390", doi = "10.1007/978-3-540-30482-1\_32", ) @book(asmbook03, author = "E. B{\"o}rger and R. F. St{\"a}rk", year = "2003", title = "Abstract State Machines---A Method for High-Level System Design and Analysis", publisher = "Springer-Verlag", doi = "10.1007/3-540-36498-6", ) @inproceedings(ButterfieldWoodcock07, author = "A. Butterfield and J. Woodcock", year = "2007", title = "{Formalising Flash Memory: First Steps}", booktitle = "Proc.~of the 12th IEEE Int.~Conf.~on Engineering Complex Computer Systems (ICECCS)", publisher = "IEEE Comp.~Soc.", address = "Washington DC, USA", pages = "251--260", doi = "10.1109/ICECCS.2007.23", ) @incollection(DamchoomButler09write, author = "K. Damchoom and M. Butler", year = "2009", title = "{Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B}", editor = "Marcel Vin\'{\i }cius Oliveira and Jim Woodcock", booktitle = "Formal Methods: Foundations and Applications", publisher = "Springer", address = "Berlin, Heidelberg", pages = "134--152", doi = "10.1007/978-3-642-10452-7\_10", ) @inproceedings(ButlerAbrial08filesystem, author = "K. Damchoom and M. Butler and J.-R. Abrial", year = "2008", title = "Modelling and Proof of a Tree-Structured File System in {E}vent-{B} and {R}odin", booktitle = "Proc. of the 10th Int.~Conf.~on Formal Methods and Sw.~Eng.~(ICFEM)", publisher = "Springer LNCS 5256", pages = "25--44", doi = "10.1007/978-3-540-88194-0\_5", ) @misc(KIV-VFS-AFS-web12, author = "G. Ernst and G. Schellhorn and D. Haneberg and J. Pf\"{a}hler and W. Reif", year = "2012", title = "{KIV models and proofs of VFS and AFS}", url = "http://www.informatik.uni-augsburg.de/swt/projects/flash.html", ) @inproceedings(Ferreira08, author = "M.A. Ferreira and S.S. Silva and J.N. Oliveira", year = "2008", title = "{Verifying Intel flash file system core specification}", booktitle = "{Modelling and Analysis in VDM: Proceedings of the Fourth VDM/Overture Workshop}", publisher = "{School of Computing Science, Newcastle University}", pages = "54--71", url = "http://twiki.di.uminho.pt/twiki/pub/Research/VFS/WebHome/overture08sl.pdf", note = "Technical Report CS-TR-1099", ) @inproceedings(Galloway-VFSmodel09, author = "A. Galloway and G. L\"{u}ttgen and J.T. M\"{u}hlberg and R.I. Siminiceanu", year = "2009", title = "Model-Checking the Linux Virtual File System", booktitle = "Proc. VMCAI'09", publisher = "Springer", pages = "74--88", doi = "10.1007/978-3-540-93900-9\_10", ) @article(Hesselink-Lali-FACS12, author = "W.H. Hesselink and M.I. Lali", year = "2012", title = "Formalizing a hierarchical file system", journal = "Form. Asp. Comput.", volume = "24", number = "1", pages = "27--44", doi = "10.1007/s00165-010-0171-2", ) @article(Hoa03, author = "C. A. R. Hoare", year = "2003", title = "The verifying compiler: A grand challenge for computing research.", journal = "J. ACM", volume = "50", number = "1", pages = "63--69", doi = "10.1007/3-540-36579-6\_19", ) @unpublished(ubifs-whitepaper08, author = "A. Hunter", year = "2008", title = "{A} Brief Introduction to the Design of {UBIFS}", url = "http://www.linux-mtd.infradead.org/doc/ubifs\_whitepaper.pdf", ) @article(Joshi-Holzmann07, author = "R. Joshi and G.J. Holzmann", year = "2007", title = "A mini challenge: build a verifiable filesystem", journal = "{Formal Aspects of Computing}", volume = "19", number = "2", doi = "10.1007/s00165-006-0022-3", ) @inproceedings(kang-jackson-flash-alloy08, author = "E. Kang and D. Jackson", year = "2008", title = "{Formal Modelling and Analysis of a Flash Filesystem in Alloy}", booktitle = "Proceedings of ABZ 2008", publisher = "Springer LNCS 5238", pages = "294 -- 308", doi = "10.1007/978-3-540-87603-8\_23", ) @incollection(MorganSufrin87, author = "C. Morgan and B. Sufrin", year = "1987", title = "Specification of the UNIX filing system", booktitle = "Specification case studies", publisher = "Prentice Hall (UK) Ltd.", address = "Hertfordshire, UK", pages = "91--140", doi = "10.1109/TSE.1984.5010215", ) @inproceedings(MarsFlashAnomaly05, author = "G. Reeves and T. Neilson", year = "2005", title = "{The Mars Rover Spirit FLASH anomaly}", booktitle = "Aerospace Conference, 2005 IEEE", pages = "4186--4199", doi = "10.1109/AERO.2005.1559723", ) @incollection(RSSB98dfgife, author = "W. Reif and G. Schellhorn and K. Stenzel and M. Balser", year = "1998", title = "Structured Specifications and Interactive Proofs with {KIV}", editor = "W. Bibel and P. Schmitt", booktitle = "{Automated Deduction---A Basis for Applications}", chapter = "1", volume = "II", publisher = "Kluwer", address = "Dordrecht", pages = "13 -- 39", url = "http://www.informatik.uni-augsburg.de/de/lehrstuehle/swt/se/publications/1998-struc\_spec\_proofs\_kiv/", note = "ISBN: 978-0-7923-5132-0", ) @inproceedings(ITL-TIME-2011, author = "G. Schellhorn and B. Tofan and G. Ernst and W. Reif", year = "2011", title = "Interleaved Programs and Rely-Guarantee Reasoning with {ITL}", booktitle = "Proc. of Temporal Representation and Reasoning (TIME)", series = "IEEE, CPS", pages = "99--106", doi = "10.1109/TIME.2011.12", ) @inproceedings(FlashFM09, author = "A. Schierl and G. Schellhorn and D. Haneberg and W. Reif", year = "2009", title = "{Abstract Specification of the UBIFS File System for Flash Memory}", booktitle = "Proceedings of FM 2009: Formal Methods", publisher = "Springer LNCS 5850", pages = "190--206", doi = "10.1007/978-3-642-05089-3\_13", ) @unpublished(fuse, author = "M. Szeredi", title = "File system in user space", url = "http://fuse.sourceforge.net", ) @misc(web:POSIX, author = "{The Open Group}", year = "2008", title = "{T}he {O}pen {G}roup {B}ase {S}pecifications {I}ssue 7, {IEEE} {S}td 1003.1, 2008 {E}dition", url = "http://www.unix.org/version3/online.html", note = "(login required)", )