Proving Theorems About JML Classes - Formal Methods and Hybrid Real-Time Systems - page 278

3. Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino,
K.R.M., Poll, E.: An overview of JML tools and applications. STTT 7(3), 212-232
(2005)
4. Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: a developer-oriented
approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805,
pp. 422-439. Springer, Heidelberg (2003)
5. Butterfield, A., Woodcock, J.: Formalising flash memory: first steps. In: 12th
IEEE International Conference on Engineering of Complex Computer Systems
(ICECCS'07), Auckland, New Zealand, July 11-14, 2007, IEEE Computer Press,
Los Alamitos (2007)
6. Cavalcanti, A.L.C.: A Refinement Calculus for Z. DPhil Thesis. University of Ox-
ford (1997)
7. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs
(1976)
8. Freitas, L., Cavalanti, A.L.C., Woodcock, J.C.P.: Taking our own medicine: apply-
ing the refinement calculus to state-rich refinement model checking. In: Liu, Z., He,
J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 697-716. Springer, Heidelberg (2006)
9. Freitas, L., et al.: Verified Software Repository @ SourceForge (2006),

vsr.sourceforge.net
10. Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z/Eves: an experiment in the
verified software repository. In: 12th IEEE International Conference on Engineering
of Complex Computer Systems (ICECCS'07), Auckland, New Zealand, July 11-14,
2007, IEEE Computer Press, Los Alamitos (2007)
11. Fu, Z.: A Refinement of the UNIX Filing System using Z/Eves. Master's thesis,
University of York (2006)
12. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd
edn. Addison Wesley, Reading (2005)
13. Hoare, T.: The Verifying Compiler Software Grand Challenge. Journal of the
ACM 50(1), 63-69 (2003)
14. Hoare, C.A.R., He, J.: Unifying Theories of Programming. International Series in
Computer Science. Prentice-Hall, Englewood Cliffs (1998)
15. Huisman, M., Jacobs, B., van den Berg, J.: A Case study in class library verifica-
tion: Java's Vector class. In: Moreira, A.M.D., Demeyer, S. (eds.) Object-Oriented
Technology. ECOOP'99 Workshop Reader. LNCS, vol. 1743, pp. 109-110. Springer,
Heidelberg (1999)
16. Huisman, M.: Reasoning about Java Programs in Higher-Order Logic using PVS
and Isabelle. PhD thesis, Universiteit Nijmegen (2001)
17. Huisman, M.: Verification of Java's AbstractCollection class: a case study. In:
Boiten, E.A., Moller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 175-194. Springer,
Heidelberg (2002)
18. IBM: CICS Application Programming Interface Release 3. Technical Report SC33-
1688-01, IBM Hursley Park (1999)
19. Intel Corp.: Open NAND Flash Interface Specification. Open NAND Flash Inter-
face Consortium (2007), http://www.onfi.org/
20. ISO/IEC 13568: Information Technology—Z Formal Specification Notation—
Syntax, Type System and Semantics. First edn. ISO/IEC (2002)
21. Josey, A. (ed.): The Single UNIX Specification Version 3. Open Group (2004),
ISBN (1931)62447X
22. Joshi, R., Holzmann, G.J.: A mini-challenge: build a verifiable filesystem. In: Veri-
fied Software: Theories, Tools, Experiments (VSTTE), IFIP Working Conference,
Zurich (In press)