Conference Papers by Ian Hayes

[1] Robert Colvin and Ian J. Hayes. CSP with hierarchical state. In Integrated Formal Methods 2009, Lecture Notes in Computer Science. Springer Verlag, 2009. Accepted. [ bib ]
[2] Steve E. Dunne, Andy J. Galloway, and Ian J. Hayes. Reasoning about loops in total and general correctness. In Unifying Theoreies of Programming 2008, Lecture Notes in Computer Science. Springer Verlag, 2008. [ bib ]
[3] Ian J. Hayes. Towards reasoning about teleo-reactive programs for robust real-time systems. In RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, pages 87-94, 2008. [ bib ]
[4] Larissa Meinicke and Ian J. Hayes. Probabilistic choice in refinement algebra. In Philippe Audebaud and Christine Paulin-Mohring, editors, Mathematics of Program Construction (MPC), volume 5133 of Lecture Notes in Computer Science, pages 243-267. Springer Verlag, 2008. [ bib | DOI | Abstract ]
[5] Cliff B. Jones, Ian J. Hayes, and Michael A. Jackson. Deriving specifications for systems that are connected to the physical world. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of Lecture Notes in Computer Science, pages 364-390. Springer Verlag, 2007. [ bib | DOI | Abstract ]
[6] L. Meinicke and I. J. Hayes. Reasoning algebraically about probabilistic loops. In Zhiming Liu and Jifeng He, editors, ICFEM, volume 4260 of LNCS, pages 380-399. Springer Verlag, 2006. [ bib | DOI | http | Abstract ]
[7] Larissa Meinicke and Ian J. Hayes. Continuous action system refinement. In T. Uustalu, editor, Mathematics of Program Construction: Proceedings 8th International Conference (MPC 2006), volume 4014 of LNCS, pages 316-337. Springer Verlag, 2006. [ bib | DOI | http | Abstract ]
[8] Ian J. Hayes. Termination of real-time programs: definitely, definitely not or maybe. In S.E. Dunne and W.J. Stoddart, editors, UTP 2006: First Int. Symp. on Unifying Theories of Programming, volume 4010 of LNCS, pages 141-154. Springer Verlag, 2006. [ bib | Abstract ]
[9] Erica Glynn, I.J. Hayes, and Anthony MacDonald. Integration of generic program analysis tools into a software development environment. In V. Estivill-Castro, editor, Computer Science 2005: Proceedings 28th Australasian Computer Science Conference (ACSC2005), volume 38 of Conferences in Research and Practice in Information Technology, pages 249-257. Australian Computer Society, 2005. [ bib | Abstract ]
[10] Cameron Smith, Kirsten Winter, I.J. Hayes, R.G. Dromey, P. Lindsay, and D.A. Carrington. An environment for building a system out of its requirements. In Proceedings 19th IEEE International Conference on Automated Software Engineering, pages 398-399. IEEE, 2004. [ bib ]
[11] I.J. Hayes. Towards platform-independent real-time systems. In P.A. Strooper, editor, ASWEC, pages 192-200. IEEE Computer Society, 2004. [ bib | Abstract ]
[12] K. Lermer, C. J. Fidge, and I. J. Hayes. Formal semantics for program paths. In J. Harland, editor, Computing: The Australian Theory Symposium (CATS) 2003, volume 78 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1-24. Elsevier, February 2003. [ bib | .html | Abstract ]
[13] I.J. Hayes. Programs as paths: An approach to timing constraint analysis. In Jin Song Dong and Jim Woodcock, editors, ICFEM, volume 2885 of LNCS, pages 1-15. Springer Verlag, 2003. [ bib | Abstract ]
[14] I.J. Hayes, M.A. Jackson, and C.B. Jones. Determining the specification of a control system from that of its environment. In K. Araki, S. Gnesi, and D. Mandrioli, editors, FME 2003: Formal Methods, volume 2805 of LNCS, pages 154-169. Springer Verlag, 2003. [ bib | .pdf | Abstract ]
[15] R. Colvin, I. J. Hayes, D. Hemer, and P.A. Strooper. Refinement of higher-order logic programs. In M. Leuschel, editor, Proceedings of the International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2002), volume 2664 of Lecture Notes in Computer Science, pages 126-143. Springer, 2003. [ bib | Abstract ]
[16] Sibylle Peuker and Ian Hayes. Reasoning about deadlines in concurrent real-time programs. In Michel Charpentier and Beverly Sanders, editors, Workshop on Formal Methods for Parallel Programming (FMPP 2003) in Proc. 17th International Parallel and Distributed Processing Symposium, pages 1-8. IEEE CS Press, 2003. [ bib | http | Abstract ]
[17] R. Colvin, I. J. Hayes, D. Hemer, and P. Strooper. Extended abstract: Refinement of higher-order logic programs. In M. Leuschel and F. Bueno, editors, Pre-Proceedings of the International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2002), pages 136-141. School of Computer Science, Technical University of Madrid, 2002. Extended abstract. [ bib ]
[18] Jamie Shield and Ian J. Hayes. Refining object-oriented invariants and dynamic constraints. In P.A. Strooper and P. Muenchaisri, editors, Asian-Pacific Software Engineering Conference (APSEC), pages 52-61. IEEE Computer Society, 2002. [ bib | http | Abstract ]
[19] S. Peuker and I.J. Hayes. Towards a refinement calculus for concurrent real-time programs. In C. George and Huaikou Miao, editors, Formal Methods and Software Engineering (ICFEM), volume 2495 of LNCS, pages 335-346. Springer-Verlag, 2002. [ bib | Abstract ]
[20] I. J. Hayes. The real-time refinement calculus: A foundation for machine-independent real-time programming. In J. Esparza and C. Lakos, editors, Proceedings 23rd International Conference on the Application and Theory of Petri Nets, volume 2360 of Lecture Notes in Computer Science, pages 44-58. Springer, 2002. Invited keynote paper. [ bib | Abstract ]
[21] I. J. Hayes. Reasoning about timeouts. In Eerke A. Boiten and Bernhard Möller, editors, Proc. Mathematics of Program Construction, volume 2386 of Lecture Notes in Computer Science, pages 94-116. Springer, 2002. [ bib | DOI | Abstract ]
[22] R. Colvin, D. Hemer, I. J. Hayes, and P. A. Strooper. Translating refined logic programs to Mercury. In M. Oudshoorn, editor, Proceedings 25th Australasian Computer Science Conference (ACSC 2002), volume 4 of Conferences in Research and Practice in Information Technology, pages 33-40. Australian Computer Society, 2002. [ bib ]
[23] D. Hemer, R. Colvin, I. Hayes, and P. Strooper. Don't care non-determinism in logic program refinement. In J. Harland, editor, Proceedings of Computing: the Australasian Theory Symposium (CATS 2002), volume 61 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1-21. Elsevier Science, 2002. [ bib | Abstract ]
[24] D. Hemer, I. Hayes, and P. Strooper. Refinement calculus for logic programming in Isabelle/HOL. In R. Boulton and P. Jackson, editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 249-264. Springer, 2001. [ bib | Abstract ]
[25] R. Colvin, I. J. Hayes, and P. Strooper. A technique for modular logic program refinement. In Kung-Kiu Lau, editor, Logic-based Program Synthesis and Transformation (LOPSTR 2000) Selected Papers, volume 2402 of Lecture Notes in Computer Science, pages 38-56. Springer, 2001. [ bib | DOI | Abstract ]
[26] J. Shield, I. J. Hayes, and D. A. Carrington. Using theory interpretation to mechanise the reals in a theorem prover. In C. J. Fidge, editor, Computing: The Australian Theory Symposium (CATS), volume 42 of Electronic Notes in Theoretical Computer Science, pages 266-281. Elsevier Science, 2001. URL: www.elsevier.nl/locate/entcs. [ bib ]
[27] I. J. Hayes. Reasoning about real-time programs using idle-invariant assertions. In J. S. Dong, J. He, and M. Purvis, editors, Proceedings 7th Asia-Pacific Software Engineering Conference (APSEC 2000), pages 16-23. IEEE Computer Society, 2000. [ bib | Abstract ]
[28] G. Smith and I. J. Hayes. Structuring real-time Object-Z specifications. In W. Grieskamp, T. Santen, and B. Stoddart, editors, IFM'00: Proceedings of the 2nd International Conference on Integrated Formal Methods, volume 1945 of Lecture Notes in Computer Science, pages 97-115. Springer, 2000. [ bib ]
[29] I. J. Hayes. Real-time program refinement using auxiliary variables. In M. Joseph, editor, Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1926 of LNCS, pages 170-184. Springer, 2000. [ bib | Abstract ]
[30] R. Colvin, I. J. Hayes, and P. Strooper. Modular logic program refinement. In Kung-Kiu Lau, editor, Pre-Proceedings of the Tenth International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2000), number UMCS-00-6-1 in Technical Report, pages 1-10. Department of Computer Science, Manchester University, 2000. Extended abstract. [ bib | Abstract ]
[31] I. J. Hayes. Reasoning about non-terminating loops using deadline commands. In R. Backhouse and J. N. Oliveira, editors, Proc. Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 60-79. Springer, 2000. This paper is superceded by [?]. [ bib | Abstract ]
[32] R. Colvin, I. J. Hayes, and P. Strooper. Refining logic programs using types. In Jenny Edwards, editor, Australasian Computer Science Conference (ACSC 2000), pages 43-50. IEEE Computer Society, 2000. [ bib | Abstract ]
[33] C. J. Fidge, I. J. Hayes, B. P. Mahony, and A. K. Wabenhorst. Real-time specification and reasoning using maximal intervals. In W. C. H. Cheng and A. S. M. Sajeev, editors, PART'99: Proceedings of the 6th Australasian Conference on Parallel and Real-Time Systems, pages 344-354. Springer, 1999. [ bib ]
[34] G. Smith and I. J. Hayes. Towards real-time Object-Z. In Keijiro Araki, Andy Galloway, and Kenji Taguchi, editors, IFM'99: Proceedings of the 1st International Conference on Integrated Formal Methods, pages 49-65. Springer, 1999. [ bib ]
[35] C. J. Fidge, I. J. Hayes, and B. P. Mahony. Defining differentiation and integration in Z. In J. Staples, M. G. Hinchey, and Shaoying Liu, editors, Proceedings Second International Conference on Formal Engineering Methods (ICFEM'98), pages 64-73. IEEE Computer Society, 1998. [ bib ]
[36] I. J. Hayes. Separating timing and calculation in real-time refinement. In J. Grundy, M. Schwenke, and T. Vickers, editors, Int. Refinement Workshop and Formal Methods Pacific 1998, pages 1-16. Springer, 1998. [ bib | .pdf | Abstract ]
[37] L. P. Wildman and I. J. Hayes. Supporting contexts in the sequential real-time refinement calculus. In J. Grundy, M. Schwenke, and T. Vickers, editors, International Refinement Workshop and Formal Methods Pacific 1998, pages 352-369. Springer, 1998. [ bib ]
[38] R. Colvin, I. J. Hayes, and P. Strooper. Data refining logic programs. In J. Grundy, M. Schwenke, and T. Vickers, editors, International Refinement Workshop and Formal Methods Pacific 1998, Discrete Mathematics and Theoretical Computer Science, pages 100-116. Springer, 1998. [ bib | Abstract ]
[39] 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, 1998. [ bib ]
[40] I. J. Hayes and M. Utting. Deadlines are termination. In D. Gries and W.-P. de Roever, editors, IFIP TC2/WG2.2, 2.3 International Conference on Programming Concepts and Methods (PROCOMET'98), pages 186-204. Chapman and Hall, 1998. [ bib | .pdf ]
[41] S. Grundon, I. J. Hayes, and C. J. Fidge. Timing constraint analysis. In C. McDonald, editor, Computer Science '98: Proc. 21st Australasian Computer Sci. Conf. (ACSC'98), pages 575-586. Springer, 1998. [ bib ]
[42] R. Colvin, I. J. Hayes, R. Nickson, and P. A. Strooper. A tool for logic program refinement. In D. J. Duke and A. S. Evans, editors, Second BCS-FACS Northern Formal Methods Workshop (NFMW'97), Electronic Workshops in Computing. Springer, 1997. [ bib ]
[43] P. G. Bancroft and I. J. Hayes. Type extension and refinement. In L. Groves and S. Reeves, editors, Formal Methods Pacific (FMP'97), pages 23-39. Springer, 1997. [ bib | Abstract ]
[44] I. J. Hayes and M. Utting. Coercing real-time refinement: A transmitter. In D. J. Duke and A. S. Evans, editors, BCS-FACS Northern Formal Methods Workshop (NFMW'96), Electronic Workshops in Computing. Springer, 1997. [ bib | .pdf ]
[45] I. Hayes, R. Nickson, and P. Strooper. Refining specifications to logic programs. In J. Gallagher, editor, Logic Program Synthesis and Transformation. Proc. of the 6th Int. Workshop, LOPSTR'96, Stockholm, Sweden, August 1996, volume 1207 of Lecture Notes in Computer Science, pages 1-19. Springer, 1997. [ bib ]
[46] I. J. Hayes and P. A. Strooper. Refining specifications to logic programs. In I.J. Hayes, editor, Proc. 5th Australasian Refinement Workshop, pages 1-13. Software Verification Research Centre, The University of Queensland, April 1996. Unrefereed. [ bib | .html ]
[47] C. J. Fidge, M. Utting, I. J. Hayes, and P. Kearney. The Quartz refinement method for real-time multi-tasking systems. In Fifth Australasian Refinement Workshop (ARW'96), April 1996. [ bib ]
[48] D. A. Carrington, I. J. Hayes, R. Nickson, G. Watson, and J. Welsh. Structured presentation of refinements and proofs. In Kotagiri Ramamohanarao, editor, Proc. 19th Australasian Computer Science Conference (ACSC'96), volume 18(1) of Australian Computer Science Communications, pages 87-96, February 1996. [ bib ]
[49] D. A. Carrington, I. J. Hayes, R. Nickson, G. Watson, and J. Welsh. A tool for developing correct programs by refinement. In He Jifeng, editor, Proc. BCS 7th Refinement Workshop, Bath, UK, Electronic Workshops in Computing, pages 1-17. Springer, 1996. [ bib ]
[50] C. J. Fidge, M. Utting, P. Kearney, and I. J. Hayes. Integrating real-time scheduling theory and program refinement. In M.-C. Gaudel and J. Woodcock, editors, FME'96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 327-346. Springer, 1996. [ bib ]
[51] I. J. Hayes. Specification models. In Proc. 7th International Conference on Putting into Practice Methods and Tools for Information Systems Design, 10-12 October, 1995, Nantes, pages 1-10, October 1995. Invited keynote paper. [ bib ]
[52] David Carrington, Ian Hayes, Ray Nickson, Geoffrey Watson, and Jim Welsh. Requirements for a program refinement engine. In Proc. of the 4th Australasian Refinement Workshop (ARW'95), pages 67-83. School of Computer Science and Engineering, University of New South Wales, April 1995. [ bib ]
[53] Ray Nickson and Ian Hayes. Program window inference. In Proc. of the 4th Australasian Refinement Workshop (ARW'95), pages 43-65. School of Computer Science and Engineering, University of New South Wales, April 1995. Unrefereed. Also available as Technical Report UQ-SVRC-95-29, Software Verification Research Centre, University of Queensland. [ bib ]
[54] L. P. Wildman and I. J. Hayes. Composing grammar transformations to construct a specification of a parser. In Ramamohanarao Kotagiri, editor, Proc. 18th Australasian Computer Science Conference (ACSC'95), Glenelg, South Australia, Australian Computer Science Communications, volume 17(1), pages 556-562, February 1995. [ bib | Abstract ]
[55] P. Bakker, D.A. Carrington, A. Goodchild, I.J. Hayes, H. Purchase, and P.A. Strooper. The communicating technologist: An educational challenge. In D. Budny and B. Herrick, editors, Frontiers in Education 25th Annual Conference, pages 4a4.1-4a4.4, Atlanta, Georgia, 1995. IEEE Press. [ bib ]
[56] P. Bancroft and I. J. Hayes. A formal semantics for a language with type extension. In ZUM'95: The Z Formal Specification Notation, Proc. 9th International Conference of Z Users, Limerick, Ireland, September 7-9, 1995, volume 967 of Lecture Notes in Computer Science, pages 299-314. Springer, 1995. [ bib ]
[57] B. P. Mahony, C. Millerchip, and I. J. Hayes. A boiler control system: Overview of a case study in timed refinement. In Diana Del Bel Belluz and Herbert C. Ratz, editors, Software Safety: Everybody's Business, Proceedings of the 1993 International Invitational Workshop on Design and Review of Software-Controlled Safety-Related Systems, Ottawa, pages 189-208. The Institute of Risk Research, 1994. [ bib ]
[58] B. P. Mahony, C. Millerchip, and I. J. Hayes. A boiler control system: A case study in timed refinement. In Diana Del Bel Belluz, editor, Technical proceedings International Symposium on Design and Review of Software-Controlled Safety-Related Systems, Ottawa, June 1993. 50 pages. [ bib | .ps ]
[59] P. Bancroft and I. J. Hayes. Refining a module with opaque types. In Gopal Gupta, George Mohay, and Rodney Topor, editors, Proceedings, 16th Australian Computer Science Conference, Brisbane, Australian Computer Science Communications, volume 15(1), pages 615-624, February 1993. [ bib ]
[60] D. A. Carrington, D. Duke, I. J. Hayes, and J. Welsh. Deriving modular designs from formal specifications. In Int. Symp. on the Foundations of Software Engineering (SIGSOFT'93), pages 89-98. ACM, 1993. [ bib | .pdf ]
[61] I. J. Hayes and L. P. Wildman. Towards libraries for Z. In J. P. Bowen and J. E. Nicholls, editors, Z User Workshop: Proceedings of the Seventh Annual Z User Meeting, London, December 1992, Workshops in Computing, pages 37-51. Springer, 1993. [ bib ]
[62] C. A. R. Hoare, I. J. Hayes, He Jifeng, C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sørensen, J. M. Spivey, and B. A. Sufrin. Laws of programming. In Manfred Broy, editor, Programming and Mathematical Method, volume 88 of NATO ASI Series F: Computer and Systems Sciences, pages 95-122. Springer, 1992. [ bib ]
[63] N. Ward and I. J. Hayes. Applications of angelic nondeterminism. In P. A. Bailes, editor, Proc. 6th Australian Software Engineering Conference (ASWEC91), pages 391-404. Australian Computer Society, July 1991. [ bib ]
[64] B. P. Mahony and I. J. Hayes. Using continuous real functions to model timed histories. In P. A. Bailes, editor, Proc. 6th Australian Software Engineering Conf. (ASWEC91), pages 257-270. Australian Comp. Soc., 1991. [ bib | .pdf ]
[65] B. P. Mahony and I. J. Hayes. A case study in timed refinement: A central heater. In Proc. BCS/FACS Fourth Refinement Workshop, Workshops in Computing, pages 138-149. Springer, January 1991. [ bib | .pdf ]
[66] I. J. Hayes. Interpretations of Z schema operators. In Z User Workshop: Proceedings of the Fifth Annual Z User Meeting, Oxford, December 1990, Workshops in Computing, pages 12-26. Springer, 1991. [ bib ]
[67] D. A. Carrington, I. J. Hayes, and J. Welsh. A syntax-directed editor for object-oriented specifications. In Proc. of Pacific TOOLS '90, pages 46-57, November 1990. [ bib ]
[68] I. J. Hayes. A generalisation of bags in Z. In J. E. Nicholls, editor, Z User Workshop: Proceedings of the Fourth Annual Z User Meeting, Oxford, December 1989, Workshops in Computing, pages 113-127. Springer, 1990. [ bib ]
[69] I. J. Hayes, M. Mowbray, and G. A. Rose. Signalling System No. 7: The network layer. In E. Brinksma, G. Scollo, and C. A. Vissers, editors, Protocol Specification, Testing and Verification, IX, pages 3-14. Elsevier Science Publishers B. V. (North-Holland), 1990. [ bib ]
[70] I. J. Hayes, R. Neucom, and J. Welsh. An editor for Z specifications. In Advance papers CASE'89, pages 1-13, 1989. [ bib ]
[71] R. Duke, I. J. Hayes, P. King, and G. A. Rose. Protocol specification and verification using Z. In IFIP Eighth International Workshop on Protocol Specification, Testing and Verification, pages 33-46. North-Holland, 1988. [ bib ]
[72] I. J. Hayes. Correctness of data representations. In Proc. 2nd Australian Software Engineering Conference (ASWEC-87), pages 75-86, Canberra, May 1987. IREE (Australia). [ bib ]
[73] G. A. Rose, R. Duke, and I. J. Hayes. Specifying communications services and protocols. In Proc 2nd Australian Software Engineering Conference (ASWEC-87), pages 161-170, Canberra, May 1987. IREE (Australia). [ bib ]
[74] I. J. Hayes. Using mathematics to specify software. In Proc. 1st Australian Software Engineering Conference (ASWEC-86), pages 67-71, Canberra, May 1986. Institution of Engineers, Australia. At the 10th ASWEC Conference in 1997 this paper was given the award of Most Influential Paper of ASWEC'86, the first ASWEC Conference. [ bib | .pdf ]
[75] I. J. Hayes. Weakest pre-specifications: weakest pre-conditions for procedures. In Proc. 9th Australian Computer Science Conference, pages 299-308, Canberra, January 1986. [ bib ]

This file has been generated by bibtex2html 1.88.

Last updated: Tue Dec 2 02:43:59 EST 2008