@ARTICLE{JH07:mini,
   author = "Joshi, Rajeev and Holzmann, Gerard",
   title = {A mini challenge: build a verifiable filesystem},
   journal = {\mbox{Formal Aspects of Computing}},
   year = 2007,
   volume = 19,
   number=2,
   pages = "269-272(4)",
   month = jun,
   note = "",
   abstract = "We propose tackling a mini challenge problem: a nontrivial verification effort that can be completed in 2-3 years, and will help establish notational standards, common formats, and libraries of benchmarks that will be essential in order for the verification community to collaborate on meeting Hoare's 15-year verification grand challenge. We believe that a suitable candidate for such a mini challenge is the development of a filesystem that is <I>verifiably</I> reliable and secure. The paper argues why we believe a filesystem is the right candidate for a mini challenge and describes a project in which we are building a small embedded filesystem for use with flash memory.",
   url = "http://eis.jpl.nasa.gov/lars/",
   doi = "doi:10.1007/s00165-006-0022-3",
}

@ARTICLE{CBO05:algtoobj,
   author = "Cruz, M. A. and Barbosa, L. S. and Oliveira, J. N.",
   title = {From Algebras to Objects: Generation and Composition},
   journal = {\mbox{Journal of Universal Computer Science}},
   year = 2004,
   volume = 11,
   number = 10,
   pages = "1580-1612(33)",
   month = oct,
   note = "",
   abstract = "This paper addresses objectification, a formal specification technique which 
inspects the potential for ob ject-orientation of a declarative model and brings the ’im- 
plicit ob jects’ explicit. Criteria for such ob jectification are formalized and implemented 
in a runnable prototype tool which embeds Vdm-sl into Vdm++. The paper also in- 
cludes a quick presentation of a (coinductive) calculus of such generated ob jects, framed 
as generalised Moore machines.",
}


@MASTERSTHESIS{S07:vdmhol,
   author = "Vermolen, Sander Dani{\"e}l",
   title = {\mbox{Automatically Discharging VDM Proof Obligations using HOL}},
   school = "Radboud University Nijmegen",
   type = "Master's thesis",
   address = "Computing Science Department",
   month = jun # "-" # aug,
   year = 2007,
   note = "",
}

@ARTICLE{W01:jffs,
   author = "Woodhouse, David",
   title = "JFFS: The Journalling File System",
   year = 2001,
}

@MISC{SITE:yaffs,
   key = "Yet Another Flash File System",
   note = "http://www.yaffs.net/",
}