[1]  Howard Chivers and Andrew Martin. Special issue on grid security. SoftwarePractice and Experience, 35(9), July 2005. 
[2]  Andrew Martin, Tolu Aina, Carl Christensen, Jamie Kettleborough, and David Stainforth. On two kinds of publicresource distributed computing. In Proceedings of Fourth UK eScience All Hands Meeting, 2005. 
[3]  D. A. Stainforth, T. Aina, C. Christensen, M. Collins, N. Faull, D. J. Frame, J. A. Kettleborough, S. Knight, A. Martin, J. M. Murphy, C. Piani, D. Sexton, L. A. Smith, R. A. Spicer, A. J. Thorpe, and M. R. Allen. Uncertainty in the predictions of the climate response to rising levels of greenhouse gases. Nature, 433:403406, 2005. 
[4]  Lee Momtahan, Andrew Martin, and A. W. Roscoe. A taxonomy of web services using CSP. In Proceedings of Web Languages and Formal Methods, 2005. [ .pdf ] 
[5]  Lee Momtahan, Andrew Martin, and A. W. Roscoe. A taxonomy of web services using CSP. Technical Report RR0422, OUCL, October 2004. [ .html ] 
[6]  Lee Momtahan and Andrew Martin. Object models: Job submission in DataGrids. Technical Report RR0426, OUCL, February 2004. [ .html ] 
[7]  Dave Stainforth, Andrew Martin, Andrew Simpson, Carl Christensen, Jamie Kettleborough, Tolu Aina, and Myles Allen. Security principles for publicresource modeling research. In 13th IEEE International Workshops on Enabling Technologies (WETICE 2004), Infrastructure for Collaborative Enterprises, 1416 June 2004, Modena, Italy, pages 319324. IEEE Computer Society, 2004. 
[8]  Andrew Martin and Carl Cook. Grids and private networks are antithetical. In Howard Chivers and Andrew Martin, editors, Grid Security Practice and Experience Workshop. Computer Science Department, University of York, YCS2004380, 2004. 
[9]  Daniel Goodman and Andrew Martin. Grid style web services for climateprediction.net. In S. Newhouse and S. Parastatidis, editors, GGF workshop on building ServiceBased Grids, Honolulu, Hawaii. Global Grid Forum, 2004. [ .pdf ] 
[10]  Jim Davies, Andrew Simpson, and Andrew Martin. Teaching formal methods in context. In C. Neville Dean and Raymond T. Boute, editors, Symposium on Teaching Formal Methods, volume 3294 of Lecture Notes in Computer Science. SpringerVerlag, 2004. 
[11]  Andrew Martin and Andrew Simpson. Generalizing the schema calculus: Database schemas and beyond. In Proceedings of 10th AsiaPacific Software Engineering Conference. IEEE press, 2003. to appear. 
[12]  Philippa Broadfoot and Andrew Martin. Grid security: Requirements and technologies a survey of the stateoftheart. Research Report PRGRR0315, Programming Research Group, Oxford University Computing LaboratoryWolfson Building, Parks Road, Oxford, OX1 3QD, UK, 2003. 
[13]  Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, and David W. Currie. ZML: XML support for Standard Z. In Didier Bert, Jonathan P. Bowen, Steve King, and Marina Waldén, editors, ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 46, 2003, Proceedings, volume 2651 of Lecture Notes in Computer Science, pages 437456. Springer, 2003. 
[14]  A C. Simpson, A. P. Martin, J. Gibbons, J. W. Davies, and S. W. McKeever. On the supervision and assessment of parttime postgraduate software engineering projects. In Proceedings of the 25th International Conference on Software Engineering (ICSE), Portland, Oregon, 310 May, 2003, pages 628633. IEEE Computer Society Press, 2003. 
[15]  Lee Momtahan and Andrew Martin. eScience experiences: Software Engineering practice and the EU DataGrid. In Proc. AsiaPacific Software Engineering Conference, pages 269275. IEEE Press, 2002. [ .pdf ] 
[16]  Andrew Martin and Lee Momtahan. eScience: A Software Engineering Challenge. Poster, 2002. UK eScience All Hands Meeting. 
[17]  D. Stainforth, J. Kettleborough, A. Martin, A. Simpson, R. Gillis, A. Akkas, R. Gault, M. Collins, D. Gavaghan, and M. Allen. Climateprediction.net: design principles for public resource modelling research. In Proc. 14th IASTED conference on parallel and distributed computing systems., 2002. 
[18]  A. Martin and C. Fidge. Lifting in Z. In Proceedings of CATS'2001, number 42 in Electronic Notes in Theoretical Computer Science, 2001. 
[19]  H. Glaser, P. H. Hartel, M. Leuschel, and A. Martin. Declarative languages in education. In Encyclopaedia of Microcomputers, volume 27, pages 79102. Marcel Dekker Inc., New York, 2000. 
[20]  S. M. Brien and A. P. Martin. A calculus for schemas in Z. J. Symbolic Computation, 30(1):6391, 2000. 
[21]  Stephen Brien and Andrew Martin. A calculus for schemas in Z. J. Symbolic Computation, 30(1):6391, 2000. 
[22]  A. P. Martin. Relating Z and firstorder logic. Formal Aspects of Computing, 12:199209, 2000. 
[23]  Andrew Martin. Relating Z and firstorder logic. In Jeanette M. Wing, Jim Woodcock, and Jim Davies, editors, FM'99  Formal Methods, number 1708,1709 in Lecture Notes in Computer Science, pages 12661280. SpringerVerlag, September 1999. 
[24] 
P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin,
A. Smith, U. UltesNitsche, and B. Walters.
Questions and answers about ten formal methods.
In S. Gnesi and D. Latella, editors, Proc. 4th Int. Workshop on
Formal Methods for Industrial Critical Systems, volume II, pages 179203,
Trento, Italy, July 1999. ERCIM, STAR/CNR, Pisa, Italy.
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.

[25]  C. J. Fidge, I. J. Hayes, A. P. Martin, and A. K. Wabenhorst. A settheoretic model for realtime specification and reasoning. In J. Jeuring, editor, Mathematics of Program Construction (MPC'98), volume 1422 of Lecture Notes in Computer Science, pages 188206. SpringerVerlag, 1998. 
[26] 
C. J. Fidge, P. Kearney, and A. P. Martin.
Applying the Cogito program development environment to realtime
system design.
In C. McDonald, editor, Computer Science '98, pages 367378.
SpringerVerlag, 1998.
Proc. 21st Australasian Computer Science Conference, Perth, 46
February 1998. Australian Computer Science Communications, Vol. 20, No. 1.
Also available as technical report SVRCTR9736.
[ http ]
This paper shows how a formal program development environment, previously used only for sequential, nonrealtime applications, can be exploited for designing parallel, realtime systems. A pragmatic approach is adopted, making best use of existing technologies, in order to quickly achieve useful results.

[27]  Owen Traynor, Dan Hazel, Peter Kearney, Andrew Martin, Ray Nickson, and Luke Wildman. The Cogito development system. In Michael Johnson, editor, Algebraic Methodology and Software Technology, volume 1349 of LNCS, pages 586591, Berlin, December 1997. SpringerVerlag. 6th International conference, AMAST'97, Sydney, Australia. 
[28] 
A. Martin, R. Nickson, and M. Utting.
A tactic language for Ergo.
In Lindsay Groves and Steve Reeves, editors, Formal Methods
Pacific '97, Springer Series in Discrete Mathematics and Theoretical
Computer Science, Singapore, May 1997. SpringerVerlag.
Also appears as TR9716, Software Verification Research Centre, The
University of Queensland, QLD 4072, Australia.
A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on 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 QuProlog. An example from classical propositional calculus is included. Keywords: tactics,user interface 
[29] 
Jon Hall and Andrew Martin.
W reconstructed.
In Jonathan P. Bowen, Michael G Hinchey, and David Till, editors,
ZUM'97: The Z Formal Specification Notation, volume 1212 of
Lecture Notes in Computer Science, Berlin Heidelberg, April 1997.
SpringerVerlag.
An early version of the Z Standard included the deductive system W for reasoning about Z specifications. Later versions contain a different deductive system. In this paper we sketch a proof that W is 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 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.

[30]  Andrew Martin. Why effective proof tool support for Z is hard. Technical Report 9734, Software Verification Research Centre, 1997. [ http ] 
[31]  Andrew Martin, Ray Nickson, and Mark Utting. Improving Angel's parallel operator: Gumtree's approach. Technical Report 9715, Software Verification Research Centre, The University of Queensland, QLD 4072, Australia, 1997. 
[32]  A. P. Martin, P. H. B. Gardiner, and J. C. P. Woodcock. A tactic calculus. Formal Aspects of Computing, 8(4):479489, 1996. An abridged version appears in the printed journal; the full version is available in the electronic supplement to Formal Aspects of Computing, 8E, pp244285. http://link.springer.de/link/service/journals/00165/supp/list94_96.htm. 
[33]  Andrew Philip Martin. Of tactics and monads. Work in progress, 1996. 
[34]  Andrew Martin. Infinite lists for specifying functional programs in Z. In Proceedings of Australian Refinement Workshop. University of Queensland, 1996. [ .ps.gz ] 
[35]  Stephen M. Brien and Andrew P. Martin. A tutorial on proof in Standard Z. Technical Monograph PRG120, Programming Research Group, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, 1995. Presented at ZUM'95. 
[36]  Andrew Martin. MachineAssisted TheoremProving for Software Engineering. D.Phil.thesis, University of Oxford, 1994. Also available as Technical Monograph PRG121, ISBN 0902928953, Oxford University Computing LaboratoryWolfson Building, Parks Road, Oxford, OX1 3QD, UK. 
[37]  Andrew Martin. Encoding W : A Logic for Z in 2OBJ. In J. C. P. Woodcock and P. G. Larsen, editors, FME'93: IndustrialStrength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 462481. SpringerVerlag, 1993. 
[38]  Andrew Martin. Infinite lists in Z. Draft paper, 1993. 
[39]  Hendrik Hilberdink and Andrew Martin. Soundness of an Encoding of W: A Logic for Z in 2OBJ. Draft report, OUCL(PRG), June 1992. 
[40]  Andrew Martin and Jeremy Gibbons. A monadic interpretation of tactics. Submitted to MPC2002. 
This file has been generated by bibtex2html 1.85.