GC6: Dependable Systems Evolution

 

Home

Publications

Book

  1. B. Meyer, J. Woodcock (eds), VSTTE: Verified Software—Theories, Tools, and Experiments, Proceedings IFIP Working Conference, ETH Zurich, 10–13 Oct 2005, LNCS 4171, Springer, 2007. 

Journal special issues

  1. JACM 2003, FACJ 2006

  2. IEEE Computer 2006

  3. Comm CSI 2007

  4. Formal Aspects of Computing 19(2).

  5. Formal Aspects of Computing 20(1).

  6. VSTTE: FACJ 19(2) , JOT 2007 , Mondex: FACJ 20(1)

  7. ICECCS: Science of Computer Programming 2008

Journal papers

  1. R. Banach, C. Jeske., M. Poppleton. and S. Stepney, Retrenching the Purse: The Balance Enquiry Quandary, and Generalised and (1, 1) Forward Refinements, Fundamenta Informaticae, 77(1-2):29-69 2007.

  2. J. Bicarregui, C. A. R. Hoare, J. Woodcock, The verified software repository: a step towards the verifying compiler, Formal Aspects of Computing Journal 18(2):143–151 2006. 

  3. A. Butterfield, L. Freitas, J. Woodcock, A mechanised model of NAND flash memory, Science of Computer Programming in press 2008. 

  4. L. Freitas, Z. Fu, J. Woodcock, A mechanically verified specification and refinement of the POSIX filestore interface, Science of Computer Programming in press 2008. 

  5. L. Freitas, K. Mokos, J. Woodcock, A mechanical verification of the CICS File Control API, Science of Computer Programming in press 2008. 

  6. L. Freitas, J. Woodcock, Mechanising Mondex with Z/EVES, Formal Aspects of Computing Journal 20(1) 2008. 

  7. C. A. R. Hoare, The Verifying Compiler: A Grand Challenge for Computing Research, Journal of the ACM 50(1):63-69, 2003.

  8. C. Jones, P. W. O’Hearn, J. Woodcock, Verified software: a grand challenge, IEEE Computer 39(4):93–95 2006. 

  9. J. Woodcock, First steps in the Verified Software Grand Challenge, IEEE Computer 39(10): 57–64 2006. 

  10. J. Woodcock, R. Banach, The Verification Grand Challenge, Computer Society of India Communications 31(2):33–36 2007. 

  11. J. Woodcock, R. Banach, The Verification Grand Challenge, Journal of Universal Computer Science 13(5):661–668 2007. 

  12. J. Woodcock, S. Stepney, D. Cooper, J. Clark, J. Jacob, The certification of the Mondex electronic purse to ITSEC Level E6, Formal Aspects of Computing 20(1) 2008. 

Conference papers

  1. E. Aydal, R. Paige, J. Woodcock, Evaluation of OCL for large-scale modelling: a different view of the Mondex smart card application, Ocl4All: Modelling Systems with OCL, MODELS’07, Nashville, Sep 2007. 

  2. R. Banach, M. Poppleton, C. Jeske, and S. Stepney, Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern, FM 2005: International Symposium of Formal Methods Europe, 18-22 July 2005.

  3. A. Butterfield, J. Woodcock, Formalising flash memory: first steps, ICECCS: 12th International Conference on Engineering of Complex Computer Systems 2006, Auckland, New Zealand, 2007. 

  4. L. Freitas, Z. Fu, J. Woodcock, POSIX filestore in Z/Eves: An experiment in the Verified Software Repository, ICECCS: 12th International Conference on Engineering of Complex Computer Systems 2006, Auckland, New Zealand, 2007. 

  5. L. Freitas, K. Mokos, J. Woodcock, Verifying the CICS File Control API with Z/Eves: An experiment in the Verified Software Repository, ICECCS: 12th International Conference on Engineering of Complex Computer Systems 2006, Auckland, New Zealand, 2007. 

  6. J. Woodcock, First steps in the Verified Software Grand Challenge, 30th Annual IEEE / NASA Software Engineering Workshop (SEW-30 2006), 203–206, 25–28 Apr 2006, Loyola College Graduate Center, Columbia, IEEE Computer Society, 2006. 

  7. J. Woodcock, Verified Software Grand Challenge, in J. Misra, T. Nipkow, E. Sekerinski (eds), FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, Aug 21-27, 2006, Proceedings, LNCS 4085:617–617, Springer, 2006. 

  8. J. Woodcock, L. Freitas, Z/Eves and the Mondex electronic purse, Theoretical Aspects of Computing — ICTAC 2006, LNCS 4281:15–34 2006. 

Technical reports

  1. T. Hoare, C. Jones, and B. Randell, Extending the Horizons of DSE (GC6). CSR Technical Report CS-TR-853, Newcastle University, 2004.
  2. G. Schellhorn, H. Grandy, D. Haneberg, and W. Reif, The Mondex Challenge: Machine Checked Proofs for an Electronic Purse, Technical Report, Institute of Computer Science, University of Augsburg, 2006.
 

Contact: jim@cs.york.ac.uk

Last updated: 6th December 2007