[1] | RobertJ. Colvin, IanJ. Hayes, and LarissaA. Meinicke. Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects of Computing, pages 1--22, 2017. Accepted 28 November 2016. [bib| Abstract] |

[2] | Julian Fell, IanJ. Hayes, and Andrius Velykis. Concurrent refinement algebra and rely quotients. Archive of Formal Proofs, December 2016. http://isa-afp.org/entries/Concurrent_Ref_Alg.shtml, Formal proof development. [bib| Abstract] |

[3] | IanJ. Hayes, RobertJ. Colvin, LarissaA. Meinicke, Kirsten Winter, and Andrius Velykis. An algebra of synchronous atomic steps. In John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, and Anna Philippou, editors, FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, volume 9995 of Lecture Notes in Computer Science, pages 352--369, Cham, November 2016. Springer International Publishing. Best paper award. [bib| DOI| http| Abstract] |

[4] | IanJ. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation. Formal Aspects of Computing, 28(6):1057--1078, November 2016. [bib| DOI| http| Abstract] |

[5] | Brijesh Dongol, IanJ. Hayes, and Georg Struth. Convolution as a unifying concept: Applications in separation logic, interval calculi, and concurrency. ACM Trans. Comput. Logic, 17(3):15:1--15:25, February 2016. [bib| DOI| http| Abstract] |

[6] | CliffB. Jones and IanJ. Hayes. Possible values: Exploring a concept for concurrency. Journal of Logical and Algebraic Methods in Programming, 2016. Accepted 8 January 2016. Available online 13 January 2016. [bib| DOI| http| Abstract] |

[7] | CliffB. Jones, IanJ. Hayes, and RobertJ. Colvin. Balancing expressiveness in formal approaches to concurrency. Formal Aspects of Computing, 27(3):475--497, May 2015. [bib| DOI| http| Abstract] |

[8] | IanJ. Hayes. Separating concerns of rely and guarantee in concurrent program derivation. In DavidA. Naumann, editor, Unifying Theories of Programming, UTP 2014, volume 8963 of LNCS, pages vii--x. Springer, 2015. [bib| Abstract] |

[9] | IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Laws and semantics for rely-guarantee refinement. Technical Report CS-TR-1425, School of Computing Science, Newcastle University, July 2014. 66 pages. [bib| Abstract] |

[10] | Brijesh Dongol, IanJ. Hayes, and PeterJ. Robinson. Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects of Computing, 26(3):563--589, May 2014. [bib| DOI| http| Abstract] |

[11] | IanJ. Hayes and Larissa Meinicke. Invariants, well-founded statements and real-time program algebra. In Cliff.B. Jones, P.Pihlajasaari, and Jun Sun, editors, Formal Methods (FM 2014), volume 8442 of LNCS, pages 318--334. Springer, 2014. [bib| Abstract] |

[12] | IanJ. Hayes. Towards structuring system specifications with time bands using layers of rely-guarantee conditions. In C.Artho and P.C. Ölveczky, editors, Formal Techniques for Safety-Critical Systems, volume 419 of Communications in Computer and Information Science, pages 1--2. Springer, 2014. [bib| DOI| Abstract] |

[13] | Brijesh Dongol, IanJ. Hayes, and John Derrick. Deriving real-time action systems with multiple time bands using algebraic reasoning. Science of Computer Programming, 85 Part B:137--165, 2014. [bib| DOI| Abstract] |

[14] | IanJ. Hayes, CliffB. Jones, and RobertJ. Colvin. Reasoning about concurrent programs: Refining rely-guarantee thinking. Technical Report CS-TR-1395, School of Computing Science, Newcastle University, September 2013. 66 pages. [bib| Abstract] |

[15] | Kirsten Winter, Chenyi Zhang, IanJ. Hayes, Nathan Keynes, Cristina Cifuentes, and Lian Li. Path-sensitive data flow analysis simplified. In Lindsay Groves and Jing Sun, editors, Formal Methods and Software Engineering: Proceedings 15th International Conference on Formal Engineering Methods (ICFEM), volume 8144 of LNCS, pages 415--430. Springer, 2013. [bib| DOI| http| Abstract] |

[16] | DanielR. Bradley and IanJ. Hayes. Visuocode: A software development environment that supports spatial navigation and composition. In Alexandru Telea, Andreas Kerren, and Andrian Marcus, editors, First IEEE Working Conference on Software Visualization (VISSOFT), pages 1--4. IEEE, 2013. [bib| DOI| http| Abstract] |

[17] | I.J. Hayes, A.Burns, B.Dongol, and C.B. Jones. Comparing degrees of non-deterministic in expression evaluation. The Computer Journal, 56(6):741--755, 2013. [bib| Abstract] |

[18] | Brijesh Dongol and IanJ. Hayes. Deriving real-time action systems in a sampling logic. Science of Computer Programming, 78(11):2047--2063, 2013. [bib| DOI| http| Abstract] |

[19] | I.J. Hayes, S.E. Dunne, and L.A. Meinicke. Linking unifying theories of program refinement. Science of Computer Programming, 78(11):2086--2107, 2013. [bib| DOI| http| Abstract] |

[20] | Brijesh Dongol, John Derrick, and IanJ. Hayes. Fractional permissions and non-deterministic evaluators in interval temporal logic. In Proc. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), volume53 of Electronic Communications of the EASST, pages 1--15, 2012. [bib| Abstract] |

[21] | Brijesh Dongol, IanJ. Hayes, Larissa Meinicke, and Kim Solin. Towards an algebra for real-time programs. In W.Kahl and T.G. Griffin, editors, 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), volume 7560 of LNCS, pages 50--65. Springer, 2012. [bib| DOI| http| Abstract] |

[22] | Brijesh Dongol and IanJ. Hayes. Deriving real-time action systems controllers from multiscale system specifications. In J.Gibbons and P.Nogueira, editors, Mathematics of Program Construction, volume 7342 of LNCS, pages 102--131. Springer, 2012. [bib| DOI| http| Abstract] |

[23] | IanJ. Hayes and RobertJ. Colvin. Integrated operational semantics: Small-step, big-step and multi-step. In John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, and Elvinia Riccobene, editors, Abstract State Machines, Alloy, B, VDM, and Z - Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, volume 7316 of LNCS, pages 21--35. Springer, 2012. [bib| DOI| Abstract] |

[24] | Brijesh Dongol and IanJ. Hayes. Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In John Derrick, Stefania Gnesi, Diego Latella, and Helen Treharne, editors, Integrated Formal Methods, volume 7321 of LNCS, pages 39--53. Springer, 2012. [bib| DOI| http| Abstract] |

[25] | Eban Escott, Paul Strooper, Paul King, and Ian Hayes. Model-driven web form validation with UML and OCL. In Andreas Harth and Nora Koch, editors, Current Trends in Web Engineering, volume 7059 of Lecture Notes in Computer Science, pages 223--235. Springer Berlin / Heidelberg, 2012. [bib| http| Abstract] |

[26] | B.Dongol and I.J. Hayes. Approximating idealised real-time specifications using time bands. In Automated Verification of Critical Systems 2011, volume46 of Electronic Communications of the EASST, pages 1--16. EASST, 2012. [bib| Abstract] |

[27] | I.J. Hayes, A.Burns, B.Dongol, and C.B. Jones. Comparing models of nondeterministic expression evaluation. Technical Report CS-TR-1273, School of Computing Science, Newcastle University, September 2011. [bib| Abstract] |

[28] | Alan Burns, Kun Wei, Jim Woodcock, IanJ. Hayes, and CliffB. Jones. Timebands framework -- 2011. Technical Report YCS-2011-467, Department of Computer Science, University of York, 2011. 36 pages. [bib| Abstract] |

[29] | R.J. Colvin and I.J. Hayes. Structural operational semantics through context-dependent behaviour. Journal of Logic and Algebraic Programming, 80(7):392--426, 2011. [bib| DOI| Abstract] |

[30] | R.J. Colvin and I.J. Hayes. A semantics for Behavior Trees using CSP with specification commands. Science of Computer Programming, 76(10):891--914, 2011. [bib| DOI| http| Abstract] |

[31] | Alan Burns and IanJ. Hayes. A timeband framework for modelling real-time systems. Real-Time Systems, 45(1--2):106--142, June 2010. [bib| DOI| http| Abstract] |

[32] | K.Winter, I.J. Hayes, and R.J. Colvin. Integrating requirements: The Behavior Tree philosophy. In J.L. Fiadeiro and S.Gnesi, editors, Proc. of Int. Conf. on Software Engineering and Formal Methods (SEFM 2010), pages 41--50. IEEE Computer Society Press, 2010. [bib| DOI| Abstract] |

[33] | I.J. Hayes. Invariants and well-foundedness in program algebra. In A.Cavalcanti, D.Déharbe, M.-C. Gaudel, and J.Woodcock, editors, International Colloquium on Theoretical Aspects of Computing (ICTAC), volume 6255 of LNCS, pages 1--14. Springer, 2010. [bib| DOI| Abstract] |

[34] | I.J. Hayes, S.E. Dunne, and L.A. Meinicke. Unifying theories of programming that distinguish nontermination and abort. In C.Bolduc, J.Desharnais, and B.Ktari, editors, Mathematics of Program Construction, volume 6120 of LNCS, pages 178--194. Springer, 2010. [bib| Abstract] |

[35] | Brijesh Dongol and IanJ. Hayes. Compositional action system derivation using enforced properties. In C.Bolduc, J.Desharnais, and B.Ktari, editors, Mathematics of Program Construction (MPC), volume 6120 of LNCS, pages 119--139. Springer Verlag, 2010. [bib| Abstract] |

[36] | SteveE. Dunne, IanJ. Hayes, and AndyJ. Galloway. Reasoning about loops in total and general correctness. In A.Butterfield, editor, Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected, volume 5713 of Lecture Notes in Computer Science, pages 62--81. Springer, 2010. [bib| DOI| Abstract] |

[37] | Brijesh Dongol and IanJ. Hayes. Enforcing safety and progress properties: An approach to concurrent program derivation. In Colin Fidge, editor, Australian Software Engineering Conference, pages 3--12. IEEE Computer Society, 2009. [bib| Abstract] |

[38] | R.J. Colvin and I.J. Hayes. CSP with hierarchical state. In M.Leuschel and H.Wehrheim, editors, Integrated Formal Methods (IFM 2009), volume 5423 of LNCS, pages 118--135. Springer, 2009. [bib| Abstract] |

[39] | IanJ. Hayes. Dynamically detecting faults via integrity constraints. In Michael Butler, Cliff Jones, Alexander Romanovsky, and Elena Troubitsyna, editors, Methods, Models, and Tools for Fault Tolerance, volume 5454 of Lecture Notes in Computer Science, pages 85--103. Springer Verlag, 2009. [bib| Abstract] |

[40] | IanJ. Hayes. Towards reasoning about teleo-reactive programs for robust real-time systems. In Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, pages 87--94, New York, NY, USA, 2008. ACM. [bib| DOI| Abstract] |

[41] | Larissa Meinicke and IanJ. 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] |

[42] | Larissa Meinicke and IanJ. Hayes. Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica, 45(5):321--382, 2008. [bib| DOI| Abstract] |

[43] | R.Colvin, I.J. Hayes, and P.A. Strooper. Calculating modules in contextual logic program refinement. Theory and Practice of Logic Programming, 8(01):1--31, 2008. [bib| DOI| arXiv| http| Abstract] |

[44] | R.Colvin and I.J. Hayes. A semantics for behavior trees. ACCS Technical Report ACCS-TR-07-01, ARC Centre for Complex Systems (ACCS), April 2007. [bib| http] |

[45] | I.J. Hayes. Procedures and parameters in the real-time program refinement calculus. Science of Computer Programming, 64(3):286--311, February 2007. [bib| DOI| Abstract] |

[46] | Brijesh Dongol and IanJ. Hayes. Trace semantics for the Owicki-Gries theory integrated with the progress logic from unity. Technical Report SSE-2007-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2007. [bib] |

[47] | C.B. Jones, I.J. Hayes, and M.A. Jackson. Deriving specifications for systems that are connected to the physical world. In C.B. Jones, Z.Liu, and J.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] |

[48] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. FACS FACTS, 2006-2:56--78, 2006. [bib] |

[49] | 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] |

[50] | Larissa Meinicke and IanJ. 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] |

[51] | I.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, 2006. [bib| Abstract] |

[52] | K.Lermer, C.J. Fidge, and I.J. Hayes. A theory for execution time derivation in real-time programs. Theoretical Computer Science, 346(1):3--27, November 2005. [bib| Abstract] |

[53] | J.Fitzgerald, I.J. Hayes, and A.Tarlecki, editors. FM 2005: Formal Methods -- Proceedings 13th International Symposium of Formal Methods Europe, Newcastle, UK, July 2005, volume 3582 of Lecture Notes in Computer Science. Springer Verlag, July 2005. [bib] |

[54] | A.Burns, I.J. Hayes, G.Baxter, and C.J. Fidge. Modelling temporal behaviour in complex socio-technical systems. Technical Report YCS390, University of York, 2005. [bib] |

[55] | 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), volume38 of Conferences in Research and Practice in Information Technology, pages 249--257. Australian Computer Society, 2005. [bib| Abstract] |

[56] | Phil Cook, Jim Welsh, and IanJ. Hayes. Building a flexible incremental compiler back-end. Technical Report SSE-2005-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib] |

[57] | Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental semantic evaluation for interactive systems: Inertia, pre-emption, and relations. Technical Report SSE-2005-01, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, 2005. [bib] |

[58] | C.Smith, K.Winter, I.J. Hayes, R.G. Dromey, P.A. Lindsay, and D.A. Carrington. An environment for building a system out of its requirements. In Proc. 19th IEEE Int. Conf. on Automated Software Engineering, pages 398--399. IEEE, 2004. [bib] |

[59] | R.Colvin, L.Groves, I.J. Hayes, D.Hemer, R.Nickson, and P.A. Strooper. Developing logic programs from specifications using stepwise refinement. In Maurice Bruynooghe and Kung-Kiu Lau, editors, Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, volume 3049 of Lecture Notes in Computer Science, pages 66--89. Springer Verlag, 2004. [bib| Abstract] |

[60] | I.J. Hayes. Towards platform-independent real-time systems. In P.A. Strooper, editor, ASWEC, pages 192--200. IEEE Computer Society, 2004. [bib| Abstract] |

[61] | K.Lermer, C.J. Fidge, and I.J. Hayes. Linear approximation of execution-time constraints. Formal Aspects of Computing, 15(4):319--348, December 2003. [bib| Abstract] |

[62] | 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, volume78 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1--24. Elsevier, February 2003. [bib| .html| Abstract] |

[63] | I.J. Hayes. Programs as paths: An approach to timing constraint analysis. In JinSong Dong and Jim Woodcock, editors, ICFEM, volume 2885 of LNCS, pages 1--15. Springer Verlag, 2003. [bib| Abstract] |

[64] | 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] |

[65] | 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] |

[66] | 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] |

[67] | I.J. Hayes. A predicative semantics for real-time refinement. In A.McIver and C.C. Morgan, editors, Programming Methodology, pages 109--133. Springer, 2003. [bib| Abstract] |

[68] | IanJ. Hayes. Block-structured (attribute) grammars. Technical Report 02-47, Software Verification Research Centre, The University of Queensland, December 2002. [bib| Abstract] |

[69] | I.J. Hayes, R.Colvin, D.Hemer, P.A. Strooper, and R.Nickson. A refinement calculus for logic programs. Theory and Practice of Logic Programming, 2(4--5):425--460, July 2002. [bib| Abstract] |

[70] | G.Smith and I.J. Hayes. An introduction to Real-Time Object-Z. Formal Aspects of Computing, 13(2):128--141, May 2002. [bib| Abstract] |

[71] | Phil Cook, Jim Welsh, and IanJ. Hayes. Incremental context-sensitive evaluation in context. Technical Report 02-11, Software Verification Research Centre, The University of Queensland, 2002. [bib] |

[72] | 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] |

[73] | Jamie Shield and IanJ. 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] |

[74] | 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--347. Springer-Verlag, 2002. [bib| Abstract] |

[75] | 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] |

[76] | I.J. Hayes. Reasoning about timeouts. In EerkeA. 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] |

[77] | R.Colvin, I.J. Hayes, D.Hemer, and P.A. Strooper. Translating refined logic programs to Mercury. In M.Oudshoorn, editor, Proceedings 25th Australasian Computer Science Conference (ACSC 2002), volume4 of Conferences in Research and Practice in Information Technology, pages 33--40. Australian Computer Society, 2002. [bib] |

[78] | 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), volume61 of Electronic Notes in Theoretical Computer Science (ENTCS), pages 1--21. Elsevier Science, 2002. [bib| Abstract] |

[79] | I.J. Hayes. Reasoning about real-time repetitions: Terminating and nonterminating. Science of Computer Programming, 43(2--3):161--192, 2002. [bib| http| .pdf| Abstract] |

[80] | I.J. Hayes, C.J. Fidge, and K.Lermer. Semantic characterisation of dead control-flow paths. IEE Proceedings---Software, 148(6):175--186, December 2001. [bib| .pdf| Abstract] |

[81] | 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] |

[82] | 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] |

[83] | I.J. Hayes and M.Utting. A sequential real-time refinement calculus. Acta Informatica, 37(6):385--448, 2001. [bib| .pdf| Abstract] |

[84] | 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), volume42 of Electronic Notes in Theoretical Computer Science, pages 266--281. Elsevier Science, 2001. URL: www.elsevier.nl/locate/entcs. [bib] |

[85] | I.J. Hayes, R.Nickson, P.Strooper, and R.Colvin. A declarative semantics for logic program refinement. Technical Report 00-30, Software Verification Research Centre, The University of Queensland, Brisbane 4072, Australia, November 2000. [bib| Abstract] |

[86] | 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] |

[87] | G.Smith and I.J. Hayes. Structuring real-time Object-Z specifications. In W.Grieskamp, T.Santen, and W.J. 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] |

[88] | 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] |

[89] | 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] |

[90] | 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 superseded by [79]. [bib| Abstract] |

[91] | R.Colvin, I.J. Hayes, and P.Strooper. Refining logic programs using types. In Jenny Edwards, editor, Australasian Computer Science Conference (ACSC2000), pages 43--50. IEEE Computer Society, 2000. [bib| Abstract] |

[92] | C.J. Fidge, I.J. Hayes, and G.Watson. The deadline command. IEE Proceedings---Software, 146(2):104--111, April 1999. [bib| .ps] |

[93] | 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] |

[94] | 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] |

[95] | I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. In J.P. Bowen and M.G. Hinchey, editors, High-Integrity System Specification and Design, pages 563--581. Springer, 1999. (Previously published in IEE/BCS Software Engineering Journal, Vol. 4, No. 6, 330--338, November, 1989). [bib] |

[96] | 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] |

[97] | 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] |

[98] | 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] |

[99] | 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] |

[100] | D.Carrington, I.Hayes, R.Nickson, G.Watson, and J.Welsh. A program refinement tool. Formal Aspects of Computing, 10(2):97--124, 1998. [bib| .ps] |

[101] | I.J. Hayes. Expressive power of specification languages. Formal Aspects of Computing, 10(2):187--192, 1998. [bib] |

[102] | 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] |

[103] | I.J. Hayes and M.Utting. Deadlines are termination. In D.Gries and W.-P. deRoever, 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] |

[104] | 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] |

[105] | 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] |

[106] | 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] |

[107] | R.Nickson and I.J. Hayes. Supporting contexts in program refinement. Science of Computer Programming, 29(3):279--302, 1997. [bib| Abstract] |

[108] | 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] |

[109] | 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] |

[110] | I.J. Hayes, editor. Proc. 5th Australasian Refinement Workshop. Software Verification Research Centre, The University of Queensland, April 1996. Unrefereed. [bib| http] |

[111] | 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] |

[112] | 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] |

[113] | 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] |

[114] | I.J. Hayes. Supporting module reuse in refinement. Science of Computer Programming, 27(2):175--184, 1996. [bib] |

[115] | 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] |

[116] | 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] |

[117] | 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] |

[118] | 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] |

[119] | 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] |

[120] | 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] |

[121] | 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] |

[122] | I.J. Hayes and J.W. Sanders. Specification by interface separation. Formal Aspects of Computing, 7(4):430--439, 1995. [bib| .pdf] |

[123] | 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] |

[124] | I.J. Hayes and B.P. Mahony. Using units of measurement in formal specifications. Formal Aspects of Computing, 7(3):329--347, 1995. [bib| .pdf] |

[125] | Report ofthe Computer Science Action LearningGroup. Improving the quality of tutorial classes in computer science. Technical Report UQ-CS-322, Department of Computer Science, University of Queensland, 1995. [bib] |

[126] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. ACM Software Engineering News, 19(3):75--81, July 1994. Unrefereed. Previously published in FACS Europe [131]. [bib] |

[127] | B.P. Mahony, C.Millerchip, and I.J. Hayes. A boiler control system: Overview of a case study in timed refinement. In Diana DelBel Belluz and HerbertC. 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] |

[128] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. Technical report UMCS-93-8-1, Department of Computer Science, University of Manchester, August 1993. [bib| .ps] |

[129] | B.P. Mahony, C.Millerchip, and I.J. Hayes. A boiler control system: A case study in timed refinement. In Diana DelBel Belluz, editor, Technical proceedings International Symposium on Design and Review of Software-Controlled Safety-Related Systems, Ottawa, June 1993. 50 pages. [bib| .ps] |

[130] | 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] |

[131] | I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the differences between VDM and Z. FACS Europe, 1(1):7--30, 1993. Unrefereed. Also published in ACM Software Engineering News, 19(3):75--81, July 1994. [bib] |

[132] | 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] |

[133] | I.J. Hayes, editor. Specification Case Studies. Prentice Hall, second edition, 1993. [bib| .pdf] |

[134] | I.J. Hayes. Examples of specification using mathematics. In I.J. Hayes, editor, Specification Case Studies, pages 2--13. Prentice Hall International, second edition, 1993. [bib] |

[135] | I.J. Hayes. Block-structured symbol table. In I.J. Hayes, editor, Specification Case Studies, pages 14--30. Prentice Hall International, second edition, 1993. [bib] |

[136] | I.J. Hayes. Flexitime specification. In I.J. Hayes, editor, Specification Case Studies, pages 134--138. Prentice Hall International, second edition, 1993. [bib] |

[137] | I.J. Hayes. Applying formal specification to software development in industry. In I.J. Hayes, editor, Specification Case Studies, pages 181--201. Prentice Hall International, second edition, 1993. (Previously published in IEEE Transactions on Software Engineering [167]). [bib] |

[138] | I.J. Hayes. CICS temporary storage. In I.J. Hayes, editor, Specification Case Studies, pages 226--237. Prentice Hall International, second edition, 1993. [bib] |

[139] | I.J. Hayes. CICS message system. In I.J. Hayes, editor, Specification Case Studies, pages 238--243. Prentice Hall International, second edition, 1993. [bib] |

[140] | 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] |

[141] | I.J. Hayes. Multi-relations in Z: A cross between multi-sets and binary relations. Acta Informatica, 29(1):33--62, February 1992. [bib| .pdf] |

[142] | B.P. Mahony and I.J. Hayes. A case-study in timed refinement: A mine pump. IEEE Trans. on Software Engineering, 18(9):817--826, 1992. [bib| .pdf] |

[143] | I.J. Hayes. VDM and Z: A comparative case study. Formal Aspects of Computing, 4(1):76--99, 1992. [bib| .pdf] |

[144] | 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, volume88 of NATO ASI Series F: Computer and Systems Sciences, pages 95--122. Springer, 1992. [bib] |

[145] | 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| .pdf] |

[146] | 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] |

[147] | 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] |

[148] | 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] |

[149] | 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] |

[150] | I.J. Hayes. Specifying physical limitations: A case study of an oscilloscope. Technical report 167, Department of Computer Science, University of Queensland, July 1990. [bib| .ps] |

[151] | I.J. Hayes. Applying formal specification to software development in industry. In RichardH. Thayer and Merlin Dorfman, editors, System and Software Requirements Engineering, pages 594--603. IEEE Computer Society Press Tutorial, 1990. (Previously published in IEEE Transactions on Software Engineering [167]). [bib] |

[152] | 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] |

[153] | 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] |

[154] | I.J. Hayes and C.B. Jones. Specifications are not (necessarily) executable. IEE/BCS Software Engineering Journal, 4(6):330--338, November 1989. [bib] |

[155] | I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. In Advance papers CASE'89, pages 1--13, 1989. [bib] |

[156] | R.Duke, I.J. Hayes, and G.A. Rose. Verification of a cyclic retransmission protocol. Technical Report UQ-CS-92, Department of Computer Science, The University of Queensland, July 1988. [bib] |

[157] | I.J. Hayes, R.Neucom, and J.Welsh. An editor for Z specifications. Technical report, Department of Computer Science, University of Queensland, 1988. [bib] |

[158] | 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] |

[159] | 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. Communications of the ACM, 30(8):672--686, August 1987. Corrigenda: CACM 30(9):770. [bib] |

[160] | 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] |

[161] | 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] |

[162] | I.J. Hayes, editor. Specification Case Studies. Prentice Hall International, 1987. [bib] |

[163] | I.J. Hayes and K.A. Robinson. A Modula-2-based translator generator. Technical report 84, Department of Computer Science, University of Queensland, Brisbane, Australia, 1987. [bib] |

[164] | 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] |

[165] | 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] |

[166] | I.J. Hayes. Specification directed module testing. IEEE Transactions on Software Engineering, SE-12(1):124--133, January 1986. [bib| .pdf] |

[167] | I.J. Hayes. Applying formal specification to software development in industry. IEEE Transactions on Software Engineering, SE-11(2):169--178, February 1985. [bib| .pdf] |

[168] | I.J. Hayes. Computer Architecture: The hardware/software interface. Ph. D. thesis, Department of Computer Science, University of New South Wales, Sydney, Australia, 1983. [bib] |

[169] | I.J. Hayes and K.A. Robinson. A tutorial on Llama: A Pascal-based translator generator. Technical report, Department of Computer Science, University of New South Wales, Sydney, Australia, 1982. [bib] |

*This file was generated by bibtex2html 1.98.*

Last updated: Sat 7 Jan 2017 15:59:07 AEDT

- ARTICLE
- ARTICLE Abstracts
- ARTICLE Bib
- BOOK
- BOOK Abstracts
- BOOK Bib
- INCOLLECTION
- INCOLLECTION Abstracts
- INCOLLECTION Bib
- INPROCEEDINGS
- INPROCEEDINGS Abstracts
- INPROCEEDINGS Bib
- PHDTHESIS
- PHDTHESIS Abstracts
- PHDTHESIS Bib
- PROCEEDINGS
- PROCEEDINGS Abstracts
- PROCEEDINGS Bib
- Pubs
- Pubs Abstracts
- Pubs Bib
- TECHREPORT
- TECHREPORT Abstracts
- TECHREPORT Bib