| [1] | Howard Chivers and Andrew Martin. Special issue on grid security. Software-Practice and Experience, 35(9), July 2005. |
| [2] | Andrew Martin, Tolu Aina, Carl Christensen, Jamie Kettleborough, and David Stainforth. On two kinds of public-resource distributed computing. In Proceedings of Fourth UK e-Science 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:403-406, 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 RR-04-22, OUCL, October 2004. [ .html ] |
| [6] | Lee Momtahan and Andrew Martin. Object models: Job submission in DataGrids. Technical Report RR-04-26, OUCL, February 2004. [ .html ] |
| [7] | Dave Stainforth, Andrew Martin, Andrew Simpson, Carl Christensen, Jamie Kettleborough, Tolu Aina, and Myles Allen. Security principles for public-resource modeling research. In 13th IEEE International Workshops on Enabling Technologies (WETICE 2004), Infrastructure for Collaborative Enterprises, 14-16 June 2004, Modena, Italy, pages 319-324. 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, YCS-2004-380, 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 Service-Based 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. Springer-Verlag, 2004. |
| [11] | Andrew Martin and Andrew Simpson. Generalizing the schema calculus: Database schemas and beyond. In Proceedings of 10th Asia-Pacific Software Engineering Conference. IEEE press, 2003. to appear. |
| [12] | Philippa Broadfoot and Andrew Martin. Grid security: Requirements and technologies a survey of the state-of-the-art. Research Report PRG-RR-03-15, 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 4-6, 2003, Proceedings, volume 2651 of Lecture Notes in Computer Science, pages 437-456. Springer, 2003. |
| [14] | A C. Simpson, A. P. Martin, J. Gibbons, J. W. Davies, and S. W. McKeever. On the supervision and assessment of part-time postgraduate software engineering projects. In Proceedings of the 25th International Conference on Software Engineering (ICSE), Portland, Oregon, 3-10 May, 2003, pages 628-633. IEEE Computer Society Press, 2003. |
| [15] | Lee Momtahan and Andrew Martin. e-Science experiences: Software Engineering practice and the EU DataGrid. In Proc. Asia-Pacific Software Engineering Conference, pages 269-275. IEEE Press, 2002. [ .pdf ] |
| [16] | Andrew Martin and Lee Momtahan. e-Science: 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 79-102. 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):63-91, 2000. |
| [21] | Stephen Brien and Andrew Martin. A calculus for schemas in Z. J. Symbolic Computation, 30(1):63-91, 2000. |
| [22] | A. P. Martin. Relating Z and first-order logic. Formal Aspects of Computing, 12:199-209, 2000. |
| [23] | Andrew Martin. Relating Z and first-order 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 1266-1280. Springer-Verlag, September 1999. |
| [24] |
P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin,
A. Smith, U. Ultes-Nitsche, 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 179-203,
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 set-theoretic model for real-time specification and reasoning. In J. Jeuring, editor, Mathematics of Program Construction (MPC'98), volume 1422 of Lecture Notes in Computer Science, pages 188-206. Springer-Verlag, 1998. |
| [26] |
C. J. Fidge, P. Kearney, and A. P. Martin.
Applying the Cogito program development environment to real-time
system design.
In C. McDonald, editor, Computer Science '98, pages 367-378.
Springer-Verlag, 1998.
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.
[ http ]
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.
|
| [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 586-591, Berlin, December 1997. Springer-Verlag. 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. Springer-Verlag.
Also appears as TR97-16, 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 Qu-Prolog. 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.
Springer-Verlag.
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 97-34, Software Verification Research Centre, 1997. [ http ] |
| [31] | Andrew Martin, Ray Nickson, and Mark Utting. Improving Angel's parallel operator: Gumtree's approach. Technical Report 97-15, 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):479-489, 1996. 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. |
| [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 PRG-120, Programming Research Group, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, 1995. Presented at ZUM'95. |
| [36] | Andrew Martin. Machine-Assisted Theorem-Proving for Software Engineering. D.Phil.thesis, University of Oxford, 1994. Also available as Technical Monograph PRG-121, ISBN 0-902928-95-3, 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: Industrial-Strength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 462-481. Springer-Verlag, 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.