Andrew Martin's publications

@ARTICLE{stainforthetal,
  AUTHOR = {D. A. Stainforth and T. Aina and C. Christensen and M. Collins and  N. Faull and D. J. Frame and J. A. Kettleborough and  S. Knight and A. Martin and J. M. Murphy and C. Piani and D. Sexton and L. A. Smith and R. A. Spicer  and A. J. Thorpe and  M. R. Allen},
  TITLE = {Uncertainty in the predictions of the climate response to rising levels of greenhouse gases},
  JOURNAL = {Nature},
  YEAR = {2005},
  VOLUME = {433},
  PAGES = {403--406},
  OPTMONTH = {January}
}

@INPROCEEDINGS{MomtahanMartin:Experiences,
  AUTHOR = {Lee Momtahan and Andrew Martin},
  TITLE = {{e-Science} Experiences: {Software Engineering} Practice and the {EU DataGrid}},
  BOOKTITLE = {Proc. Asia-Pacific Software Engineering Conference},
  YEAR = 2002,
  PAGES = {269--275},
  PUBLISHER = {IEEE Press}
}

@INPROCEEDINGS{stainforth:security,
  AUTHOR = {Dave Stainforth and
               Andrew Martin and
               Andrew Simpson and
               Carl Christensen and
               Jamie Kettleborough and
               Tolu Aina and
               Myles Allen},
  TITLE = {Security Principles for Public-Resource Modeling Research.},
  BOOKTITLE = {WETICE},
  YEAR = {2004},
  PAGES = {319-324},
  EE = {http://doi.ieeecomputersociety.org/10.1109/ENABL.2004.54},
  CROSSREF = {DBLP:conf/wetice/2004},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}

@PROCEEDINGS{DBLP:conf/wetice/2004,
  TITLE = {13th IEEE International Workshops on Enabling Technologies
               (WETICE 2004), Infrastructure for Collaborative Enterprises,
               14-16 June 2004, Modena, Italy},
  BOOKTITLE = {WETICE},
  PUBLISHER = {IEEE Computer Society},
  YEAR = {2004},
  ISBN = {0-7695-2183-5},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}

@PROCEEDINGS{DBLP:conf/wetice/2004,
  TITLE = {13th IEEE International Workshops on Enabling Technologies
               (WETICE 2004), Infrastructure for Collaborative Enterprises,
               14-16 June 2004, Modena, Italy},
  BOOKTITLE = {WETICE},
  PUBLISHER = {IEEE Computer Society},
  YEAR = {2004},
  ISBN = {0-7695-2183-5},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{MartinCook,
  AUTHOR = {Andrew Martin and Carl Cook},
  TITLE = {Grids and Private Networks are Anthitetical},
  BOOKTITLE = {Grid Security Practice and Experience Workshop},
  YEAR = {2004},
  EDITOR = {Howard Chivers and Andrew Martin},
  PUBLISHER = {Computer Science Department, University of York, YCS-2004-380}
}

@MISC{MartinMomtahan:Challenge,
  AUTHOR = {Andrew Martin and Lee Momtahan},
  TITLE = {{e-Science}: A {Software Engineering Challenge}},
  BOOKTITLE = {UK eScience All Hands Meeting},
  NOTE = {UK eScience All Hands Meeting},
  YEAR = 2002,
  HOWPUBLISHED = {Poster}
}

@INPROCEEDINGS{soton:tenmethods,
  AUTHOR = {P. Hartel and M. Butler and A. Currie and P. Henderson and
    M. Leuschel and A. Martin and A. Smith and U. Ultes-Nitsche and
    B. Walters},
  TITLE = {Questions and Answers About Ten Formal Methods },
  BOOKTITLE = {Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems },
  ABSTRACT = {An abstract model of an industrial distributed data base application has been studied using process based, state based, and queueing theory based methods. The methods supported by graphical notations and/or integrated development environments were found to be easiest to work with. The methods supported by model checkers were the most successful in obtaining relevant information about the application. Applying a number of different methods to study one particular model encourages a problem to be viewed from different angles. This gives complementary information about the model. We report on a variety of problems of the model found through various routes. Our main conclusion is that asking experts to apply different methods and tools at a sufficiently abstract level can be done effectively revealing a broad range of information about the considered application. 
},
  PAGES = {179-203 },
  YEAR = { 1999 },
  EDITOR = { S. Gnesi and D. Latella},
  VOLUME = {  II },
  ADDRESS = { Trento, Italy },
  MONTH = { July },
  ORGANIZATION = { ERCIM },
  PUBLISHER = { STAR/CNR, Pisa, Italy },
  ISBN = { 88-7958-009-4 }
}

@INPROCEEDINGS{GoodmanMartin,
  AUTHOR = {Daniel Goodman and Andrew Martin},
  TITLE = {Grid Style Web Services for climate\emph{prediction}.net},
  BOOKTITLE = {GGF workshop on building Service-Based Grids, Honolulu, Hawaii},
  YEAR = {2004},
  EDITOR = {S. Newhouse and S. Parastatidis},
  ORGANIZATION = {Global Grid Forum}
}

@INCOLLECTION{declarative,
  AUTHOR = {H. Glaser and P. H. Hartel and  M. Leuschel and A. Martin},
  TITLE = {Declarative languages in education},
  BOOKTITLE = {Encyclopaedia of Microcomputers},
  OPTCROSSREF = {},
  OPTKEY = {},
  PAGES = {79--102},
  PUBLISHER = {Marcel Dekker Inc.},
  YEAR = { 2000 },
  OPTEDITOR = {},
  VOLUME = {27},
  OPTNUMBER = {},
  OPTSERIES = {},
  OPTTYPE = {},
  OPTCHAPTER = {},
  ADDRESS = {New York},
  OPTEDITION = {},
  OPTMONTH = {},
  NOTE = {}
}

@ARTICLE{BM:schemas,
  AUTHOR = {S. M. Brien and A. P. Martin},
  TITLE = {A Calculus for Schemas in {Z}},
  JOURNAL = {J. Symbolic Computation},
  YEAR = {2000},
  OPTKEY = {},
  VOLUME = {30},
  NUMBER = {1},
  PAGES = {63--91},
  OPTMONTH = {},
  OPTNOTE = {},
  OPTANNOTE = {}
}

@TECHREPORT{me:proof-is-hard,
  TITLE = {Why effective proof tool support for {Z} is hard},
  AUTHOR = {Andrew Martin},
  INSTITUTION = {Software Verification Research Centre},
  NUMBER = {97-34},
  YEAR = {1997},
  URL = {http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?97-34}
}

@INPROCEEDINGS{MNU:TacErgo,
  TITLE = {A Tactic Language for {Ergo}},
  KEYWORDS = {tactics,user interface},
  AUTHOR = {A. Martin and R. Nickson and M. Utting},
  MONTH = {May},
  YEAR = {1997},
  ABSTRACT = { A new version of the Ergo theorem prover is under
                  development. It uses a single tactic language, based
                  on \emph{Angel}, for tactic programming, user
                  interface, and proof representation. This paper
                  describes the language as it is used in each of
                  these cases, and explains the details of its
                  implementation in Qu-Prolog. An example from
                  classical propositional calculus is included. },
  CROSSREF = {FMP97},
  NOTE = {Also appears as TR97-16, Software Verification
                  Research Centre, The University of Queensland, QLD
                  4072, Australia}
}

@PROCEEDINGS{FMP97,
  EDITOR = {Lindsay Groves and Steve Reeves},
  TITLE = {Formal Methods Pacific '97},
  BOOKTITLE = {Formal Methods Pacific '97},
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {Singapore},
  SERIES = {Springer Series in Discrete Mathematics and 
		 Theoretical Computer Science},
  YEAR = 1997,
  MONTH = JUL,
  ISBN = {981-3083-31-X}
}

@TECHREPORT{MNU:parallel,
  AUTHOR = {Andrew Martin and Ray Nickson and Mark Utting},
  TITLE = {Improving {Angel}'s Parallel Operator: {Gumtree}'s
                  Approach},
  INSTITUTION = {Software Verification Research Centre},
  ADDRESS = {The University of Queensland, QLD 4072, Australia},
  YEAR = 1997,
  NUMBER = {97-15}
}

@TECHREPORT{BM:tutorial,
  AUTHOR = {Stephen M. Brien and Andrew P. Martin},
  TITLE = {A Tutorial on Proof in {Standard Z}},
  TYPE = {Technical Monograph},
  NUMBER = {PRG-120},
  YEAR = 1995,
  ISBN = {0-902928-94-5},
  INSTITUTION = {Programming Research Group, Oxford University Computing Laboratory},
  ADDRESS = {Wolfson Building, Parks Road, Oxford, OX1 3QD, UK},
  NOTE = {Presented at ZUM'95}
}

@PHDTHESIS{me:thesis,
  AUTHOR = {Andrew Martin},
  TITLE = {Machine-Assisted Theorem-Proving for Software
                  Engineering},
  TYPE = {{D.Phil.}\ Thesis},
  YEAR = 1994,
  MONTH = {Michaelmas},
  SCHOOL = {University of Oxford},
  NOTE = {Also available as Technical Monograph PRG-121, ISBN
                  0-902928-95-3, Oxford University Computing LaboratoryWolfson Building, Parks Road, Oxford, OX1 3QD, UK}
}

@TECHREPORT{W&2OBJ:soundness,
  AUTHOR = {Hendrik Hilberdink and Andrew Martin},
  TITLE = {{Soundness of an Encoding of \Wlog: A Logic for Z in
                  2OBJ}},
  TYPE = {Draft Report},
  INSTITUTION = {OUCL(PRG)},
  YEAR = {1992},
  MONTH = {June}
}

@INPROCEEDINGS{apm:ew2o,
  AUTHOR = {Andrew Martin},
  TITLE = {{Encoding \Wlog : A Logic for Z in 2OBJ}},
  CROSSREF = {FME93},
  PAGES = {462--481}
}

@PROCEEDINGS{FME93,
  EDITOR = {J. C. P. Woodcock and P. G. Larsen},
  TITLE = {FME'93: Industrial-Strength Formal Methods},
  BOOKTITLE = {FME'93: Industrial-Strength Formal Methods},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1993,
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 670,
  ISBN = {0-387-56662-7 and 3-540-56662-7}
}

@UNPUBLISHED{apm:infZ,
  AUTHOR = {Andrew Martin},
  TITLE = {Infinite Lists in {Z}},
  YEAR = 1993,
  NOTE = {Draft paper}
}

@INPROCEEDINGS{HallMartin:WReconstructed,
  AUTHOR = {Jon Hall and Andrew Martin},
  TITLE = {W Reconstructed},
  CROSSREF = {zum97},
  YEAR = 1997,
  MONTH = APR,
  ABSTRACT = { An early version of the Z Standard included the
                  deductive system ${\cal W}$ for reasoning about Z
                  specifications. Later versions contain a different
                  deductive system. In this paper we sketch a proof
                  that $\cal W$ is \emph{relatively sound} with
                  respect to this new deductive system. We do this by
                  demonstrating a semantic basis for a correspondence
                  between the two systems, then showing that each of
                  the inference rules of $\cal W$ can be simulated as
                  derived rules in the new system. These new rules are
                  presented as tactics over the the inference rules of
                  the new deductive system. }
}

@PROCEEDINGS{zum97,
  TITLE = {{ZUM'97}: The {Z} Formal Specification Notation,
	      10th International Conference of {Z} Users, 
	      {Reading}, {UK}, April 1997, Proceedings},
  BOOKTITLE = {{ZUM'97}: The {Z} Formal Specification Notation},
  EDITOR = {Jonathan P. Bowen and Michael G Hinchey and David Till},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1212,
  ADDRESS = {Berlin Heidelberg},
  YEAR = 1997,
  ISBN = {3-540-62717-0},
  ANNOTE = {10th International Conference of Z Users, 
	       University of Reading, April 1997, Proceedings}
}

@ARTICLE{MGW:Tactics,
  AUTHOR = {A. P. Martin and P. H. B. Gardiner and
                  J. C. P. Woodcock},
  TITLE = {A Tactic Calculus},
  YEAR = {1996},
  VOLUME = 8,
  NUMBER = 4,
  PAGES = {479--489},
  JOURNAL = {Formal Aspects of Computing},
  PUBLISHER = {Springer--Verlag},
  NOTE = {An abridged version appears in the printed journal;
                  the full version is available in the electronic
                  supplement to Formal Aspects of Computing, 8E, pp244--285.
http://link.springer.de/link/service/journals/00165/supp/list94\_96.htm},
  ABSTACT = { We present a very general language for expressing
                  tactic programs. The paper describes some essential
                  tactic combinators (tacticals), and gives them a
                  formal semantics. Those definitions are used to
                  produce a complete calculus for reasoning about
                  tactics written in this language. The language is
                  extended to cover {\em structural combinators} which
                  enable the tactics to be precisely targeted upon
                  particular sub-expressions.}
}

@UNPUBLISHED{Martin:Monads,
  AUTHOR = {Andrew Philip Martin},
  TITLE = {Of Tactics and Monads},
  NOTE = {Work in progress},
  YEAR = 1996
}

@INPROCEEDINGS{Us:CogDev,
  AUTHOR = {Owen Traynor and Dan Hazel and Peter Kearney and
                  Andrew Martin and Ray Nickson and Luke Wildman},
  TITLE = {The {Cogito} development system},
  PAGES = {586--591},
  CROSSREF = {AMAST97}
}

@PROCEEDINGS{AMAST97,
  EDITOR = {Michael Johnson},
  TITLE = {Algebraic Methodology and Software Technology},
  BOOKTITLE = {Algebraic Methodology and Software Technology},
  SERIES = {LNCS},
  VOLUME = 1349,
  YEAR = 1997,
  MONTH = DEC,
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {Berlin},
  ISBN = {3-540-63888-1},
  ISSN = {0302-9743},
  SUBJECTCLASSIF = {D.3-4,D.2,C.3,D.1.6,I.2.3,H.2.1-4},
  NOTE = {6th International conference, AMAST'97, Sydney, Australia}
}

@INPROCEEDINGS{fidge:mpc98,
  AUTHOR = {C. J. Fidge and I. J. Hayes and A. P. Martin and
                  A. K. Wabenhorst},
  TITLE = {A Set-Theoretic Model for Real-Time Specification
                  and Reasoning},
  EDITOR = {J. Jeuring},
  BOOKTITLE = {Mathematics of Program Construction (MPC'98)},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1422,
  YEAR = 1998,
  PAGES = {188--206},
  COMMENT = {Also available as SVRC TR 98-7}
}

@INPROCEEDINGS{fkm98,
  AUTHOR = {C. J. Fidge and P. Kearney and A. P. Martin},
  TITLE = {Applying the {Cogito} Program Development
                  Environment to Real-Time System Design},
  EDITOR = {C. McDonald},
  BOOKTITLE = {Computer Science '98},
  PUBLISHER = {Springer-Verlag},
  PAGES = {367--378},
  YEAR = 1998,
  ISBN = {981-3083-90-5},
  ABSTRACT = {This paper shows how a formal program development
                  environment, previously used only for sequential,
                  non-real-time applications, can be exploited for
                  designing parallel, real-time systems. A pragmatic
                  approach is adopted, making best use of existing
                  technologies, in order to quickly achieve useful
                  results.},
  NOTE = {Proc. 21st Australasian Computer Science Conference,
                  Perth, 4-6 February 1998. Australian Computer
                  Science Communications, Vol. 20, No. 1. Also
                  available as technical report SVRC-TR-97-36.},
  URL = {http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?97-36}
}

@INPROCEEDINGS{me:infinite,
  AUTHOR = {Andrew Martin},
  TITLE = {Infinite Lists for Specifying Functional Programs in
                  {Z}},
  YEAR = 1996,
  BOOKTITLE = {Proceedings of Australian Refinement Workshop},
  URL = {http://www.it.uq.edu.au/MENU/WORKSHOPS-SEMINARS-CONFERENCES/WORKSHOPS/Martin.ps.gz},
  PUBLISHER = {University of Queensland}
}

@ARTICLE{BrienMartin:Calculus,
  AUTHOR = {Stephen Brien and Andrew Martin},
  TITLE = {A calculus for schemas in {Z}},
  JOURNAL = {J. Symbolic Computation},
  YEAR = 2000,
  VOLUME = 30,
  NUMBER = 1,
  PAGES = {63--91}
}

@INPROCEEDINGS{APM:Relating-FM,
  AUTHOR = {Andrew Martin},
  TITLE = {Relating {Z} and first-order logic},
  CROSSREF = {FM99},
  PAGES = {1266--1280}
}

@PROCEEDINGS{FM99,
  TITLE = {FM'99 -- Formal Methods},
  BOOKTITLE = {FM'99 -- Formal Methods},
  YEAR = {1999},
  EDITOR = {Jeanette M. Wing and Jim Woodcock and Jim Davies},
  NUMBER = {1708,1709},
  SERIES = {Lecture Notes in Computer Science},
  MONTH = SEP,
  PUBLISHER = {Springer-Verlag}
}

@INPROCEEDINGS{cpdn-arch,
  AUTHOR = {Stainforth, D. and Kettleborough, J. and
                  Martin, A. and  Simpson, A. and  Gillis, R. and
                  Akkas, A. and Gault, R. and Collins, M. and 
                  Gavaghan, D. and Allen, M.},
  TITLE = {Climate\emph{prediction}.net: 
                   design principles for public resource modelling research.},
  BOOKTITLE = {Proc. 14th IASTED conference on parallel and distributed
computing systems.},
  YEAR = {2002}
}

@INPROCEEDINGS{martinfidge:lifting,
  AUTHOR = {A. Martin and C. Fidge},
  TITLE = {Lifting in {Z}},
  BOOKTITLE = {Proceedings of CATS'2001},
  YEAR = {2001},
  SERIES = {Electronic Notes in Theoretical Computer Science},
  NUMBER = 42
}

@ARTICLE{APM:Relating-FACS,
  AUTHOR = {A. P. Martin},
  TITLE = {Relating {Z} and First-order logic},
  JOURNAL = {Formal Aspects of Computing},
  YEAR = {2000},
  VOLUME = {12},
  PAGES = {199--209}
}

@UNPUBLISHED{monads-tactics,
  AUTHOR = {Andrew Martin and Jeremy Gibbons},
  TITLE = {A Monadic Interpretation of Tactics},
  NOTE = {Submitted to MPC2002 }
}

@INPROCEEDINGS{MartinSimpsonZDB,
  AUTHOR = {Andrew Martin and Andrew Simpson},
  TITLE = {Generalizing the Schema Calculus: Database Schemas and Beyond},
  BOOKTITLE = {Proceedings of 10th Asia-Pacific Software Engineering Conference},
  YEAR = {2003},
  PUBLISHER = {IEEE press},
  NOTE = {to appear}
}

@TECHREPORT{broadfootMartin:grid-sec,
  AUTHOR = {Philippa Broadfoot and Andrew Martin},
  TITLE = {Grid Security: Requirements and Technologies
A Survey of the State-of-the-art},
  YEAR = 2003,
  TYPE = {Research Report},
  INSTITUTION = {Programming Research Group},
  ADDRESS = {Oxford University Computing LaboratoryWolfson Building, Parks Road, Oxford, OX1 3QD, UK},
  NUMBER = {PRG-RR-03-15}
}

@INPROCEEDINGS{zml,
  AUTHOR = {Mark Utting and Ian Toyn and Jing Sun and Andrew Martin
		and Jin Song Dong and Nicholas Daley and David W. Currie},
  TITLE = {{ZML}: {XML} Support for {Standard Z}},
  PAGES = {437-456},
  CROSSREF = {DBLP:conf/zum/2003}
}

@PROCEEDINGS{DBLP:conf/zum/2003,
  EDITOR = {Didier Bert and
               Jonathan P. Bowen and
               Steve King and
               Marina Wald{\'e}n},
  TITLE = {ZB 2003: Formal Specification and Development in Z and B, 
Third
               International Conference of B and Z Users, Turku, Finland, 
June
               4-6, 2003, Proceedings},
  BOOKTITLE = {ZB},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2651},
  YEAR = {2003},
  ISBN = {3-540-40253-5},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}

@INPROCEEDINGS{whatever,
  AUTHOR = {Simpson, A~C. and Martin, A.~P. and Gibbons, J. and 
          Davies, J.~W. and McKeever, S.~W.},
  TITLE = {On the supervision and assessment of 
part-time postgraduate software engineering projects},
  YEAR = {2003},
  PAGES = {628--633},
  PUBLISHER = {{IEEE} Computer Society Press},
  BOOKTITLE = {Proceedings of the 25th International Conference 
on Software  Engineering (ICSE), Portland, Oregon, 3--10 May, 2003}
}

@INPROCEEDINGS{Daviesetal,
  AUTHOR = {Jim Davies and Andrew Simpson and Andrew Martin},
  TITLE = {Teaching Formal Methods in Context},
  BOOKTITLE = {Symposium on Teaching Formal Methods},
  PAGES = {},
  YEAR = {2004},
  EDITOR = {C. Neville Dean and Raymond T. Boute},
  VOLUME = {3294},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag}
}

@PROCEEDINGS{DBLP:conf/zum/2003,
  EDITOR = {Didier Bert and
               Jonathan P. Bowen and
               Steve King and
               Marina Wald{\'e}n},
  TITLE = {ZB 2003: Formal Specification and Development in Z and B, 
Third
               International Conference of B and Z Users, Turku, Finland, 
June
               4-6, 2003, Proceedings},
  BOOKTITLE = {ZB},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2651},
  YEAR = {2003},
  ISBN = {3-540-40253-5},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}

@PROCEEDINGS{FME93,
  EDITOR = {J. C. P. Woodcock and P. G. Larsen},
  TITLE = {FME'93: Industrial-Strength Formal Methods},
  BOOKTITLE = {FME'93: Industrial-Strength Formal Methods},
  PUBLISHER = {Springer-Verlag},
  YEAR = 1993,
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 670,
  ISBN = {0-387-56662-7 and 3-540-56662-7}
}

@PROCEEDINGS{FM99,
  TITLE = {FM'99 -- Formal Methods},
  BOOKTITLE = {FM'99 -- Formal Methods},
  YEAR = {1999},
  EDITOR = {Jeanette M. Wing and Jim Woodcock and Jim Davies},
  NUMBER = {1708,1709},
  SERIES = {Lecture Notes in Computer Science},
  MONTH = SEP,
  PUBLISHER = {Springer-Verlag}
}

@PROCEEDINGS{AMAST97,
  EDITOR = {Michael Johnson},
  TITLE = {Algebraic Methodology and Software Technology},
  BOOKTITLE = {Algebraic Methodology and Software Technology},
  SERIES = {LNCS},
  VOLUME = 1349,
  YEAR = 1997,
  MONTH = DEC,
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {Berlin},
  ISBN = {3-540-63888-1},
  ISSN = {0302-9743},
  SUBJECTCLASSIF = {D.3-4,D.2,C.3,D.1.6,I.2.3,H.2.1-4},
  NOTE = {6th International conference, AMAST'97, Sydney, Australia}
}

@PROCEEDINGS{FMP97,
  EDITOR = {Lindsay Groves and Steve Reeves},
  TITLE = {Formal Methods Pacific '97},
  BOOKTITLE = {Formal Methods Pacific '97},
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {Singapore},
  SERIES = {Springer Series in Discrete Mathematics and 
		 Theoretical Computer Science},
  YEAR = 1997,
  MONTH = JUL,
  ISBN = {981-3083-31-X}
}

@PROCEEDINGS{zum97,
  TITLE = {{ZUM'97}: The {Z} Formal Specification Notation,
	      10th International Conference of {Z} Users, 
	      {Reading}, {UK}, April 1997, Proceedings},
  BOOKTITLE = {{ZUM'97}: The {Z} Formal Specification Notation},
  EDITOR = {Jonathan P. Bowen and Michael G Hinchey and David Till},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 1212,
  ADDRESS = {Berlin Heidelberg},
  YEAR = 1997,
  ISBN = {3-540-62717-0},
  ANNOTE = {10th International Conference of Z Users, 
	       University of Reading, April 1997, Proceedings}
}