Emeritus Professor Ian Hayes

Featured projects	Duration
Design and verification of correct, efficient and secure concurrent systems ARC Discovery Project	2019–2022
Verifying GraalVM Optimization Passes	2020–2026

Evangelou-Oost, Naso, Meinicke, Larissa, Bannister, Callum and Hayes, Ian J. (2023). Trace Models of Concurrent Valuation Algebras. Formal Methods and Software Engineering. (pp. 118-136) Singapore: Springer Nature Singapore. doi: 10.1007/978-981-99-7584-6_8

Hayes, Ian J., Jones, Cliff B. and Meinicke, Larissa A. (2023). Specifying and reasoning about shared-variable concurrency. Theories of programming and formal methods. (pp. 110-135) edited by Jonathan P. Bowen, Qin Li and Qiwen Xu. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-40436-8_5

Hayes, Ian J. and King, Steve (2021). Software specification. Theories of programming: the life and works of Tony Hoare. (pp. 251-270) edited by Cliff B. Jones and Jayadev Misra. New York, NY USA: Association for Computing Machinery. doi: 10.1145/3477355.3477367

Hayes, Ian J. (2009). Dynamically detecting faults via integrity constraints. Methods, Models, and Tools for Fault Tolerance. (pp. 85-103) edited by Michael Butler, Cliff Jones, Alexander Romanovsky and Elena Troubitsyna. Berlin, Germany: Springer Verlag. doi: 10.1007/978-3-642-00867-2_5

Jones, C. B., Hayes, I. J. and Jackson, M. A. (2007). Deriving specifications for systems that are connected to the physical world. Formal Methods and Hybrid Real-Time Systems. (pp. 364-390) edited by Jones, C. B., Liu, Z. and Woodcock, J.. Berlin, Germany: Springer-Verlag. doi: 10.1007/978-3-540-75221-9_16

Colvin, Robert, Groves, Lindsay, Hayes, Ian J., Hemer, David, Nickson, Ray and Strooper, Paul (2004). Developing logic programs from specifications using stepwise refinement. Program Development in Computational Logic. (pp. 66-89) edited by Maurice Bruynooghe and Kunk-Kiu Lau. Berlin: Springer Verlag. doi: 10.1007/978-3-540-25951-0_3

Hayes, I. J. (2003). A predicative semantics for real-time refinement. Programming Methodology. (pp. 109-133) edited by A. McIver and C. Morgan. New York: Springer Verlag. doi: 10.1007/978-0-387-21798-7_6

Hayes, I. J. and Jones, C. B. (1999). Specifications are not (necessarily) executable. High-integrity system specification and design. (pp. 563-581) edited by J. P. Bowen and M. G. Hinchey. London: Springer.

Hayes, I. J. and Utting, M. (1998). Deadlines are termination. Programming Concepts and Methods PROCOMET ’98. (pp. 186-204) Boston, MA, United States: Springer. doi: 10.1007/978-0-387-35358-6_15

Dongol, Brijesh, Hayes, Ian J. and Struth, Georg (2021). Convolution algebras: relational convolution, generalised modalities and incidence algebras. Logical Methods in Computer Science, 17 (1) 13, 1-34. doi: 10.23638/LMCS-17(1:13)2021

Burns, Alan, Hayes, Ian J. and Jones, Cliff B. (2019). Deriving specifications of control programs for cyber physical systems. The Computer Journal, 63 (5), 774-790. doi: 10.1093/comjnl/bxz019

Hayes, Ian J., Meinicke, Larissa A., Winter, Kirsten and Colvin, Robert J. (2018). A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects of Computing, 31 (2), 133-163. doi: 10.1007/s00165-018-0464-4

Colvin, Robert J., Hayes, Ian J. and Meinicke, Larissa A. (2017). Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects of Computing, 29 (5), 1-23. doi: 10.1007/s00165-017-0416-4

Jones, Cliff B. and Hayes, Ian J. (2016). Possible values: exploring a concept for concurrency. Journal of Logical and Algebraic Methods in Programming, 85 (5 Part 2), 972-984. doi: 10.1016/j.jlamp.2016.01.002

Hayes, Ian J. (2016). Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects of Computing, 28 (6), 1057-1078. doi: 10.1007/s00165-016-0384-0

Dongol, Brijesh, Hayes, Ian J. and Struth, Georg (2016). Convolution as a unifying concept: applications in separation logic, interval calculi, and concurrency. ACM Transactions on Computational Logic, 17 (3) 15, 1-25. doi: 10.1145/2874773

Jones, Cliff B., Hayes, Ian J. and Colvin, Robert J. (2014). Balancing expressiveness in formal approaches to concurrency. Formal Aspects of Computing, 27 (3), 1-23. doi: 10.1007/s00165-014-0310-2

Dongol, Brijesh, Hayes, Ian J. and Derrick, John (2014). Deriving real-time action systems with multiple time bands using algebraic reasoning. Science of Computer Programming, 85 (PART B), 137-165. doi: 10.1016/j.scico.2013.08.009

Dongol, Brijesh, Hayes, Ian J. and Robinson, Peter J. (2014). Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects of Computing, 26 (3), 563-589. doi: 10.1007/s00165-012-0272-1

Hayes, Ian J., Dunne, Steve E. and Meinicke, Larissa A. (2013). Linking unifying theories of program refinement. Science of Computer Programming, 78 (11), 2086-2107. doi: 10.1016/j.scico.2012.07.010

Dongol, Brijesh and Hayes, Ian J. (2013). Deriving real-time action systems in a sampling logic. Science of Computer Programming, 78 (11), 2047-2063. doi: 10.1016/j.scico.2012.07.008

Hayes, Ian J., Burns, Alan, Dongol, Brijesh and Jones, Cliff B. (2013). Comparing degrees of non-Determinism in expression evaluation. Computer Journal, 56 (6), 741-755. doi: 10.1093/comjnl/bxt005

Höfner, Peter, Van Glabbeek, Rob and Hayes, Ian (2012). Preface: Morgan: a suitable case for treatment. Formal Aspects of Computing, 24 (4-6), 417-422. doi: 10.1007/s00165-012-0257-0

Colvin, Robert J. and Hayes, Ian J. (2011). Structural operational semantics through context-dependent behaviour. Journal of Logic and Algebraic Programming, 80 (7), 392-426. doi: 10.1016/j.jlap.2011.05.001

Colvin, Robert J. and Hayes, Ian J. (2011). A semantics for Behavior Trees using CSP with specification commands. Science of Computer Programming, 76 (10), 891-914. doi: 10.1016/j.scico.2010.11.007

Burns, Alan and Hayes, Ian J. (2010). A timeband framework for modelling real-time systems. Real-time Systems [computer resource], 45 (1-2), 106-142. doi: 10.1007/s11241-010-9094-5

Meinicke, Larissa and Hayes, Ian J. (2008). Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica, 45 (5), 321-382. doi: 10.1007/s00236-008-0073-4

Colvin, Robert, Hayes, Ian J. and Strooper, Paul A. (2008). Calculating modules in contextual logic program refinement. Theory and Practice of Logic Programming, 8 (1), 1-31. doi: 10.1017/S1471068407003043

Hayes, I. J. (2007). Procedures and parameters in the real-time program refinement calculus. Science of Computer Programming, 64 (3), 286-311. doi: 10.1016/j.scico.2006.06.002

Lermer, Karl, Fidge, Colin J. and Hayes, Ian J. (2005). A theory for execution-time derivation in real-time programs. Theoretical Computer Science, 346 (1), 3-27. doi: 10.1016/j.tcs.2005.08.003

Lermer, K. R. C., Fidge, C. J. and Hayes, I. J. (2003). Linear approximation of execution-time constraints. Formal Aspects of Computing, 15 (4), 319-348. doi: 10.1007/s00165-003-0019-0

Shield, J. and Hayes, I. J. (2002). Refining object-oriented invariants and dynamic constraints. Proceedings - Asia-Pacific Software Engineering Conference, APSEC 1182975, 52-61. doi: 10.1109/APSEC.2002.1182975

Hayes, Ian (2002). Reasoning about real-time repetitions: terminating and nonterminating. Science of Computer Programming, 43 (2-3), 161-192. doi: 10.1016/S0167-6423(02)00024-2

Hayes, Ian, Colvin, Robert, Hemer, David, Strooper, Paul and Nickson, Ray (2002). A refinement calculus for logic programs. Theory And Practice of Logic Programming, 2 (Part 4-5), 425-460. doi: 10.1017/S1471068402001448

Hayes, I. J., Fidge, C. J. and Lermer, K. R. C. (2001). Semantic characterisation of dead control-flow paths. IEE Proceedings Software, 148 (6), 175-186. doi: 10.1049/ip-sen:20010834

Hayes, I. J. and Utting, M. (2001). A sequential real-time refinement calculus. Acta Informatica, 37 (6), 385-448. doi: 10.1007/PL00013311

Fidge, C. J., Hayes, I. J. and Watson, G. N. (1999). The deadline command. IEE Proceedings - Software, 146 (2), 104-111. doi: 10.1049/ip-sen:19990407

Hayes, Ian J. (1998). Expressive Power of Specification Languages. Formal Aspects of Computing, 10 (2), 187-192. doi: 10.1007/s001650050010

Carrington D., Hayes I., Nickson R., Watson G. and Welsh J. (1998). A Program Refinement Tool. Formal Aspects of Computing, 10 (2), 97-124. doi: 10.1007/s001650050006

Nickson, R and Hayes, I (1997). Supporting contexts in program refinement. Science of Computer Programming, 29 (3), 279-302. doi: 10.1016/S0167-6423(97)00002-6

Hayes I.J. (1996). Supporting module reuse in refinement. Science of Computer Programming, 27 (2), 175-184. doi: 10.1016/0167-6423(96)00006-8

Hayes, I. J. and Sanders, J. W. (1995). Specification by interface separation. Formal Aspects of Computing, 7 (4), 430-439. doi: 10.1007/bf01211217

Hayes, Ian J. and Mahony, Brendan P. (1995). Using units of measurement in formal specifications. Formal Aspects of Computing, 7 (3), 329-347. doi: 10.1007/bf01211077

Hayes, Ian (1992). Multi-relations in Z: A cross between multi-sets and binary relations. Acta Informatica, 29 (1), 33-62. doi: 10.1007/BF01178565

Mahony B.P. and Hayes I.J. (1992). A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering, 18 (9), 817-826. doi: 10.1109/32.159841

Hayes, Ian (1992). VDM and Z: A comparative case study. Formal Aspects of Computing, 4 (1), 76-99. doi: 10.1007/bf01214957

Hayes, Ian J. (1991). Case studies in systematic software development. Science of Computer Programming, 17 (1-3), 250-251. doi: 10.1016/0167-6423(91)90042-v

Hayes, Ian J. (1991). The semantics of programming languages: An elementary introduction using structural operational semantics. Science of Computer Programming, 16 (3), 278-279. doi: 10.1016/0167-6423(91)90011-l

Hoare, C. A.R., Hayes, I. J., Jifeng, He, Morgan, C. C., Roscoe, A. W., Sanders, J. W., Sorensen, I. H., Spivey, J. M. and Sufrin, B. A. (1987). Laws of programming. Communications of the ACM, 30 (8), 672-686. doi: 10.1145/27651.27653

Hayes, Ian J. (1986). Specification directed module testing. IEEE Transactions on Software Engineering, SE-12 (1), 124-133. doi: 10.1109/tse.1986.6312926

Hayes, Ian J. (1985). APPLYING FORMAL SPECIFICATION TO SOFTWARE DEVELOPMENT IN INDUSTRY. IEEE Transactions on Software Engineering, SE-11 (2), 169-178. doi: 10.1109/TSE.1985.232191

Hayes, Ian J. (1978). Some remarks on "Ambiguous Machine Architecture". ACM SIGARCH Computer Architecture News, 6 (8), 23-24. doi: 10.1145/1216467.1216473

Utting, Mark, Webb, Brae J. and Hayes, Ian J. (2023). Differential testing of a verification framework for compiler optimizations (Case study). IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC Australia, 14-15 May 2023. Piscataway, NJ United States: Institute of Electrical and Electronics Engineers.. doi: 10.1109/formalise58978.2023.00015

Meinicke, Larissa A. and Hayes, Ian J. (2023). Using cylindric algebra to support local variables in rely/guarantee concurrency. IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC, Australia, 14-15 May 2023. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/formalise58978.2023.00019

Webb, Brae J., Hayes, Ian J. and Utting, Mark (2023). Verifying term graph optimizations using Isabelle/HOL. 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'23), Boston, MA, United States, 16-17 January 2023. New York, NY, United States: ACM. doi: 10.1145/3573105.3575673

Hayes, Ian J., Utting, Mark and Webb, Brae J. (2023). Verifying compiler optimisations (invited paper). 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, 21–24 November 2023. Singapore, Singapore: Springer Nature Singapore. doi: 10.1007/978-981-99-7584-6_1

Evangelou-Oost, Nasos, Bannister, Callum and Hayes, Ian J. (2023). Contextuality in distributed systems. 20th International Conference, RAMiCS 2023, Augsburg, Germany, 3-6 April 2023. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-031-28083-2_4

Webb, Brae J., Utting, Mark and Hayes, Ian J. (2021). A formal semantics of the GraalVM intermediate representation. 19th International Symposium, ATVA 2021, Gold Coast, QLD Australia, 18-22 October 2021. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-88885-5_8

Dongol, Brijesh, Hayes, Ian, Meinicke, Larissa and Struth, Georg (2019). Cylindric Kleene Lattices for Program Construction. MPC: 13th International Conference on Mathematics of Program Construction, Porto, Portugal, 7–9 October 2019. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-33636-3_8

Hayes, Ian J. and Meinicke, Larissa A. (2019). Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges. UTP: 7th International Symposium on Unifying Theories of Programming, Porto, Portugal, 8 October 2019. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-31038-7_9

Hayes, Ian J. and Jones, Cliff B. (2018). A guide to rely/guarantee thinking. Third International School, SETSS 2017, Chongqing, China, 17–22 April 2017. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-02928-9_1

Hayes, Ian J. (2018). Some challenges of specifying concurrent program components. 18th Refinement Workshop, Refine 2018, Oxford, United Kingdom, 18 July 2018. SYDNEY: Open Publishing Association. doi: 10.4204/EPTCS.282.2

Hayes, Ian J. and Meinicke, Larissa A. (2018). Encoding fairness in a synchronous concurrent program algebra. 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 15-17 July 2018. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-95582-7_13

Hayes, Ian J. (2018). Engineering a theory of concurrent programming. 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, 12-16 November 2018. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-02450-5_1

Wu, Xi, Lu, Yi, Meiring, Patrick A., Hayes, Ian J. and Meinicke, Larissa A. (2018). Type capabilities for object-oriented programming languages. 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD Australia, 12-16 November 2018. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-02450-5_13

Hayes, Ian J., Wu, Xi and Meinicke, Larissa A. (2017). Capabilities for Java: Secure access to resources. 15th Asian Symposium on Programming Languages and Systems, APLAS 2017, Suzhou, People's Republic of China, 27-29 November 2017. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-71237-6_4

Hayes, Ian J., Colvin, Robert J., Meinicke, Larissa A., Winter, Kirsten and Velykis, Andrius (2016). An algebra of synchronous atomic steps. 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, 9-11 November 2016. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-48989-6_22

Hayes, Ian J. (2015). Separating concerns of rely and guarantee in concurrent program derivation. Unifying Theories of Programming: 5th International Symposium, Singapore, 13 May, 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-14806-9

Hayes, Ian J. and Meinicke, Larissa (2014). Invariants, well-founded statements and real-time program algebra. 19th International Symposium on Formal Methods, FM 2014, Singapore, 12 - 16 May 2014. Heidelberg, Germany: Springer Verlag. doi: 10.1007/978-3-319-06410-9_23

Hayes, Ian J. (2014). Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions. 2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013, Queenstown, 29 - 30 October 2013. Springer Verlag. doi: 10.1007/978-3-319-05416-2_1

Bradley, Daniel R. and Hayes, Ian J. (2013). Visuocode: A software development environment that supports spatial navigation and composition. 1st IEEE Working Conference on Software Visualization, VISSOFT 2013, Eindhoven, The Netherlands, 27 - 28 September 2013. Piscatawa, NJ United States: I E E E. doi: 10.1109/VISSOFT.2013.6650533

Winter, Kirsten, Zhang, Chenyi, Hayes, Ian J., Keynes, Nathan, Cifuentes, Cristina and Li, Lisa (2013). Path-sensitive data flow analysis simplified. 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, 29 October - 1 November 2013. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-41202-8_27

Dongol, Brijesh, Hayes, Ian J., Meinicke, Larissa and Solin, Kim (2012). Towards an algebra for real-time programs. 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012), Cambridge, United Kingdom, 17 - 20 September 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-33314-9_4

Dongol, Brijesh and Hayes, Ian J. (2012). Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. 9th International Conference on Integrated Formal Methods (IFM 2012), Pisa, Italy, 18-21 June 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-30729-4_4

Escott, Eban, Strooper, Paul, King, Paul and Hayes, Ian J. (2012). Model-driven web form validation with UML and OCL. 11th International Conference on Web Engineering (ICWE 2011), Paphos, Cyprus, 20-21 June 2011. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-27997-3_23

Hayes, Ian J. and Colvin, Robert J. (2012). Integrated operational semantics: small-step, big-step and multi-step. 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), Pisa, Italy, 18-21 June 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-30885-7_2

Dongol, Brijesh and Hayes, Ian J. (2012). Deriving real-time action systems controllers from multiscale system specifications. Mathematics of Program Construction 11th International Conference, MPC 2012, Madrid, Spain, 25 - 27 June 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-31113-0_7

Dongol, Brijesh, Derrick, John and Hayes, Ian J. (2012). Fractional permissions and non-deterministic evaluators in interval temporal logic. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Bamberg, Germany, 18–20 September 2012. Berlin, Germany: European Association of Software Science and Technology (E A S S T). doi: 10.14279/tuj.eceasst.53.792.791

Dongol, Brijesh and Hayes, Ian J. (2011). Approximating idealised real-time specifications using time bands. 11th International Workshop on Automated Verification of Critical Systems, Newcastle upon Tyne, United Kingdom, 12-14 September 2011. Berlin, Germany: European Association of Software Science and Technology. doi: 10.14279/tuj.eceasst.46.684.701

Dongol, Brijesh and Hayes, Ian J. (2010). Compositional action system derivation using enforced properties. Mathematics of Program Construction [MPC], Quebec City, Quebec, Canada, 21-23 June, 2010. Berlin, Germany: Springer. doi: 10.1007/978-3-642-13321-3_9

Hayes, I. J., Dunne, S. E. and Meinicke, L. (2010). Unifying theories of programming that distinguish nontermination and abort. Mathematics of Program Construction [MPC], Québec City, Québec, Canada, 21-23 June, 2010. Berlin, Germany: Springer. doi: 10.1007/978-3-642-13321-3

Winter, Kirsten, Hayes, Ian J. and Colvin, Robert (2010). Integrating requirements: The behavior tree philosophy. Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, 13-18 September 2010. United States: IEEE Computer Society. doi: 10.1109/SEFM.2010.13

Hayes, Ian J. (2010). Invariants and well-foundedness in program algebra. 7th International Colloquium on Theoretical Aspects of Computing (ICTAC 2010), Natal, Rio Grande do Norte, Brazil, 1-3 September 2010. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-14808-8_1

Dunne, Steve E., Hayes, Ian J. and Galloway, Andy J. (2010). Reasoning about loops in total and general correctness. Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, 8-10 September, 2008. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-14521-6_5

Hayes, Ian J. (2009). Dynamically detecting faults via integrity constraints. doi: 10.1007/978-3-642-00867-2_5

Colvin, Robert and Hayes, Ian J. (2009). CSP with hierarchical state. 7th International Conference on Integrated Formal Methods: IFM 2009, Dusseldorf, Germany, 16-19 February 2009. New York , U.S.A: Springer-Verlag. doi: 10.1007/978-3-642-00255-7_9

Dongol, Brijesh and Hayes, Ian J. (2009). Enforcing safety and progress properties: An approach to concurrent program derivation. Australian Software Engineering Conference [ASWEC], Gold Coast , Australia, 14-17 April 2009. Los Alamitos, CA, U.S.A.: IEEE Computer Society. doi: 10.1109/ASWEC.2009.12

Hayes, I.J. (2008). Towards reasoning about teleo-reactive programs for robust real-time systems. 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems (SERENE '08), Newcastle Upon Tyne, UK, 17-19 Nov 2008. New York , U.S.A.: ACM. doi: 10.1145/1479772.1479789

Meinicke, L. and Hayes, I. J. (2008). Probabilistic Choice in Refinement Algebra. 9th International Conference on Mathematics of Program Construction [MPC], Marseille, France, 15-18 July 2008. Berlin, Heidelberg: Springer Verlag. doi: 10.1007/978-3-540-70594-9_14

Meinicke, Larissa and Hayes, Ian J. (2006). Reasoning algebraically about probabilistic loops. 8th International Conference on Formal Engineering Methods, Macua, PR China, 1-3 November, 2006. Berlin, Germany: Springer-Verlag. doi: 10.1007/11901433_21

Hayes, I. J. (2006). Termination of real-time programs: definitely, definitely not, or maybe. First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, 5 - 7 February, 2006. Heidelberg, Germany: Springer Verlag. doi: 10.1007/11768173_9

Meinicke, L. A. and Hayes, I. J. (2006). Continuous action system refinement. 8th International Conference on Mathematics of Program Construction (MPC 2006), Kuressaare, Estonia, 3-5 July 2006. Berlin, Germany: Springer-Verlag. doi: 10.1007/11783596_19

Glynn, Erica, Hayes, Ian and MacDonald, Anthony (2005). Integration of generic program analysis tools into a software development environment.

Lermer, Karl, Fidge, Colin J. and Hayes, Ian J. (2005). A theory for execution-time derivation in real-time programs. doi: 10.1016/j.tcs.2005.08.003

Glynn, Erica, Hayes, Ian and Macdonald, Anthony (2005). Integration of generic program analysis tools into a software development environment. Twenty-Eighth Australasian Conference Computer Science, Newcastle, NSW, 31 Jan - 3 Feb 2005. Sydney: Australian Computer Society.

Smith, C., Winter, K., Hayes, I., Dromey, G., Lindsay, P. and Carrington, D. (2004). An environment for building a system out of its requirements. Proceedings - 19th International Conference on Automated Software Engineering, ASE 2004, , , September 20, 2004-September 24, 2004. doi: 10.1109/ASE.2004.1342775

Hayes, I. J. (2004). Towards platform-independent real-time systems. The 2004 Australian Software Engineering Conference (ASWEC 2004), Melbourne, Australia, 13-16 April 2004. Los Alamitos, California, U.S.A.: IEEE Computer Society. doi: 10.1109/ASWEC.2004.1290472

Lermer, Karl, Fidge, Colin and Hayes, Ian J. (2003). Formal Semantics for Program Paths. Computing: The Australasian Theory Symposium [CATS], Adelaide, 4-7 February 2003. Amsterdam ; New York: Elsevier Science. doi: 10.1016/S1571-0661(04)81006-5

Peuker, S. and Hayes, I. J. (2003). Reasoning about deadlines in concurrent real-time programs. International Parallel and Distributed Processing Symposium 2003, Nice, France, 22-26 April 2003. Los Alamitos, CA, U.S.A.: IEEE Computer Society. doi: 10.1109/IPDPS.2003.1213430

Hayes, I. J., Jackson, M. A. and Jones, C. B. (2003). Determining the specification of a control system from that of its environment. International Symposium of Formal Methods Europe, Pisa, Italy, 8-14 September 2003. Berlin: Springer Verlag. doi: 10.1007/978-3-540-45236-2_10

Hayes, I. J. (2003). Programs as paths: An approach to timing constraint analysis. The Fifth International Conference on Formal Engineering Methods, Singapore, 5-7 November 2003. Germany: Springer. doi: 10.1007/978-3-540-39893-6_1

Colvin, Robert, Hayes, Ian J., Hemer, David G. and Strooper, Paul A. (2003). Refinement of higher-order logic programs. The Twelfth International Symposium on Logic-based Program Synthesis and Transformation, Madrid, Spain, 17-20 September 2002. Berlin: Springer. doi: 10.1007/3-540-45013-0_11

Hayes, Ian (2002). Reasoning about real-time repetitions: Terminating and nonterminating. doi: 10.1016/S0167-6423(02)00024-2

Colvin, R., Hayes, I. J., Hemer, D. G. and Strooper, P. A. (2002). Translating refined logic programs to Mercury. ACSC 2002, Melbourne, Australia, 28 January - 1 February, 2002. Sydney, Australia: Australian Computer Society Inc..

Hayes, I. J. (2002). The real-time refinement calculus: A foundation for machine-independent real-time programming. Application and Theory of Petri Nets 2002, 23rd International Conference ICATPN, Adelaide, Australia, 24-30 June 2002. Berlin: Springer-Verlag. doi: 10.1007/3-540-48068-4_3

Hayes, I. J. (2002). Reasoning about timeouts. Sixth International Conference, MPC 2002, Dagstuhl, Germany, 8-10 July, 2002. Berlin: Springer-Verlag. doi: 10.1007/3-540-45442-X_7

Smith, G. P. and Hayes, I. J. (2002). An introduction to real-time Object-Z. London: Springer-Verlag. doi: 10.1007/s001650200003

Shield, J. and Hayes, I. J. (2002). Refining object-orientated invariants and dynamic constraints. Ninth Asia-Pacific Software Engineering Conference, The Gold Coast, 4-6 December, 2002. Los Alamitos, California: IEEE Computer Society.

Hemer, David, Colvin, Robert, Hayes, Ian and Strooper, Paul (2002). Don't care non-determinism in logic program refinement. CATS'02, Computing: the Australasian Theory Symposium, Amsterdam, Denmark, 28 January - 1 February 2002. Amsterdam ; New York: Elsevier Science. doi: 10.1016/S1571-0661(04)00308-1

Peuker, S. and Hayes, I. J. (2002). Towards a refinement calculus for concurrent real-time programs. ICFEM 2002, Shanghai, China, 21-25th October, 2002. Heidelberg: Springer-Verlag. doi: 10.1007/3-540-36103-0_35

Shield, J., Hayes, I. J. and Carrington, D. A. (2001). Using theory interpretation to mechanise the reals in a theorem prover. CATS2001, Gold Coast, 29 January-1 February, 2001. Oxford: Elsevier.

Shield, Jamie, Hayes, Ian and Carrington, David (2001). Using theory interpretation to mechanise the reals in a theorem prover. Computing: The Australasian Theory Symposium (CATS 2001), , , January 29, 2001-January 30, 2001. Elsevier. doi: 10.1016/S1571-0661(04)80890-9

Hemer, David, Hayes, Ian and Strooper, Paul (2001). Refinement Calculus for Logic Programming in Isabelle/HOL. TPHOLs: International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, UK, 3–6 September 2001 . Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-44755-5_18

Hemer, David, Hayes, Ian and Strooper, Paul (2001). Refinement calculus for logic programming in Isabelle/HOL. Springer Verlag.

Colvin, Robert, Hayes, Ian and Strooper, Paul (2001). A technique for modular logic program refinement. Tenth International Workshop on Logic-Based Program Synthesis and Transformation, London, England, 24-28 July, 2001. Berlin: Springer-Verlag. doi: 10.1007/3-540-45142-0_3

Hayes, I. J. (2000). Reasoning about real-time programs using idle-invariant assertions. APSEC 2000, Singapore, 5-8 December 2000. Washington: IEEE Computer Society. doi: 10.1109/APSEC.2000.896678

Hayes, I. J. (2000). Real-time program refinement using auxiliary variables. Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, Pune, India, 20-22 September 2000. Berlin, Germany: Springer. doi: 10.1007/3-540-45352-0_15

Hayes, I. J. (2000). Reasoning about non-terminating loops using deadline commands. MPC 2000, Ponte de Lima, Portugal, 3-5 July 2000. Berlin: Springer. doi: 10.1007/10722010_5

Smith, G and Hayes, I (2000). Structuring real-time Object-Z specifications. Integrated Formal Methods: Second International Conference, IFM 2000,, Dagstuhl Castle, Germany, November 2000. Berlin, Germany: Springer. doi: 10.1007/3-540-40911-4_7

Colvin, Robert, Hayes, Ian J. and Strooper, Paul A. (2000). Refining logic programs using types. ACSC 2000, Canberra, ACT, Australia, 31 January - 3 February, 2000. Los Alamitos, CA, USA: IEEE Computer Society. doi: 10.1109/ACSC.2000.824379

Smith, G. P. and Hayes, I. J. (1999). Towards real-time Object-Z. Integrated Formal Methods IFM'99, York, UK, 28-29 June 1999. London: Springer-Verlag. doi: 10.1007/978-1-4471-0851-1_4

Fidge, C. J., Hayes, I. J., Mahony, B. and Wabenhorst, A. K. (1999). Real-time specification and reasoning using maximal intervals. PART '99, Melbourne, Australia, 29 Nov - 1 Dec 1999. Singapore: Springer-Verlag.

Fidge, C. J., Hayes, I. J. and Mahony, B. P. (1998). Defining differentiation and integration in Z. 2nd International Conference on Formal Engineering Methods, ICFEM 1998, Brisbane, QLD, December 9, 1998-December 11, 1998. Institute of Electrical and Electronics Engineers Inc.. doi: 10.1109/ICFEM.1998.730571

Fidge, C. J., Hayes, I. J., Martin, A. P. and Wabenhorst, A. K. (1998). A set-theoretic model for real-time specification and reasoning. 4th International Conference on Mathematics of Program Construction, MPC 1998, Marstrand, June 15- 17 1998. Germany: Springer Verlag. doi: 10.1007/bfb0054291

Colvin, R., Hayes, I. J. and Strooper, P. (1998). Data refining logic programs. International Refinement Workshop and Formal Methods Pacific '98, Canberra, Australia, 29 September - 2 October, 1998. New York: Springer -Verlag.

Colvin, R., Hayes, I., Nickson, R. and Strooper, P. (1997). A tool for logic program refinement (Extended abstract). Formal Methods Pacific Conference (FMP 97), Wellington New Zealand, 9-11 July 1997. Singapore: Springer-Verlag Singapore Pte..

Hayes, Ian and Utting, Mark (1996). Coercing real-time refinement: a transmitter. BCS-FACS Northern Formal Methods Workshop, Ilkley, United Kingdom, 23-24 September 1996. BCS Learning & Development. doi: 10.14236/ewic/fa1996.9

Hayes, I. J., Nickson, R. G. and Strooper, P. A. (1996). Refining specifications to logic programs. Logic Program Synthesis and Transformation 6th International Workshop, LOPSTR'96, Stockholm, Sweden, August 28–30, 1996. Berlin / Heidelberg: Spinger. doi: 10.1007/3-540-62718-9_1

Fidge, C., Utting, M., Kearney, P. and Hayes, I. (1996). Integrating real-time scheduling theory and program refinement. 3rd International Symposium of Formal Methods Europe, FME 1996, Oxford, United Kingdom, 18-22 March 1996. Springer Verlag. doi: 10.1007/3-540-60973-3_95

Bakker Paul, Carrington David, Goodchild Andrew, Hayes Ian, Purchase Helen and Strooper Paul (1995). Communicating technologist: an educational challenge. Proceedings of the 1995 25th Annual Conference on Frontiers in Education. Part 1 (of 2), Atlanta, GA, USA, November 1, 1995-November 4, 1995. doi: 10.1109/fie.1995.483173

Bancroft, Peter and Hayes, Ian (1995). A formal semantics for a language with type extension. 9th International Conference of Z Users Meeting, ZUM 1995, Limerick Ireland, 7- 9 September 1995. Germany: Springer Verlag.

Hayes, I., Araki, K., Duke, D. and Veraart, V. (1995). Are formal methods relevant?. Institute of Electrical and Electronics Engineers Inc.. doi: 10.1109/APSEC.1995.497003

Hayes, Ian and Wildman, Luke (1993). Towards Libraries for Z. Z User Workshop, London 1992, London, United Kingdom, 14–15 December 1992. London: Springer London. doi: 10.1007/978-1-4471-3556-2_3

Carrington, David, Duke, David, Hayes, Ian and Welsh, Jim (1993). Deriving modular designs from formal specifications. 1st ACM SIGSOFT Symposium on Foundations of Software Engineering, SIGSOFT 1993, Los Angeles, CA, 8 - 10 December 1993. New York, NY United States: Association for Computing Machinery. doi: 10.1145/256428.167066

Hayes, Ian (1991). Interpretations of Z Schema Operators. Z User Workshop, Oxford 1990 , Oxford United Kingdom, 17–18 December 1990. London: Springer London. doi: 10.1007/978-1-4471-3540-1_2

Mahony, Brendan and Hayes, Ian (1991). A Case Study in Timed Refinement: A Central Heater. 4th Refinement Workshop, Cambridge, United Kingdom, 9–11 January 1991. London: Springer London. doi: 10.1007/978-1-4471-3756-6_8

Hayes, Ian (1990). A Generalisation of Bags in Z. Z User Workshop , Oxford, , 15 December 1989. London: Springer London. doi: 10.1007/978-1-4471-3877-8_7

Hayes I.J. (1986). Using mathematics to specify software. First Australian Software Engineering Conference. Software Engineering: Path to Computer Systems Reliability, Canberra, Aust, *. Inst of Engineers.

Dongol, Brijesh M.S., Hayes, Ian J. and Robinson, Peter J. (2013). Prolog. The University of Queensand. (Dataset) doi: 10.14264/uql.2014.173

Dongol, Brijesh and Hayes, Ian J. (2011). Reasoning about teleo-reactive programs under parallel composition. Technical Report SSE, 2011-01. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Colvin, Robert and Hayes, Ian J. (2010). A semantics for behavior trees. Systems and Software Engineering Technical Reports, SSE-2010-03. School of Information Technol and Elec Engineering, University of Queensland.

Colvin, Robert and Hayes, Ian J. (2010). Structural operational semantics through context-dependent behaviour. Systems and Software Engineering Technical Reports, SSE-2010-02. School of Information Technology and Electrical Engineering, The University of Queensland.

Dongol, Brijesh, Hayes, Ian J. and Robinson, Peter J. (2009). Reasoning about real-time teleo-reactive programs. Technical Report SSE-2010-01. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Brijesh Dongol and Ian J. Hayes (2007). Trace Semantics for the Owicki-Gries Theory Integrated with the Progress Logic from UNITY. SSE Technical Reports, Technical Report SSE-2007-02. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Hayes, Ian J. and Meinicke, Larissa (2006). Reasoning Algebraically about Probabilistic Loops. Technical Report SSE-2006-02. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Meinicke, Larissa and Hayes, Ian J. (2006). Algebraic Reasoning for Probabilistic Action Systems and While-Loops. Technical Report SSE-2006-05. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Cook, Phil, Welsh, Jim and Hayes, Ian J. (2005). 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.

Cook, Phil, Welsh, Jim and Hayes, Ian J. (2005). 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.

Lermer, Karl, Fidge, Colin and Hayes, Ian (2002). Linear Approximation of Execution Time Constraints. Technical Report 02-31. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Peuker, Sibylle and Hayes, Ian (2002). Timing Analysis of Concurrent Real-Time Programs With Deadlines. Technical Report 02-37. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Cook, Phil, Welsh, Jim and Hayes, Ian J. (2002). Incremental Context-Sensitive Evaluation in Context. Technical Report 02-11. Software Verification Research Centre, The University of Queensland.

Lermer, Karl, Fidge, Colin and Hayes, Ian (2002). A Theory for Execution Time Derivation in Real-time Programs. Technical Report 02-13. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Lermer, Karl, Fidge, Colin and Hayes, Ian (2002). Formal Semantics for Program Paths. Technical Report 02-05. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Colvin, Robert, Hemer, David, Hayes, Ian and Strooper, Paul (2001). Translating Refined Logic Programs to Mercury. Technical Report no. 01-32. Software Verification Research Centre, School of Information Technology, The University Of Queensland.

Hemer, D. G., Colvin, R., Hayes, I. J. and Strooper, P. A. (2001). Don't care non-determinism in logic program refinement. SRV Techical Report No. 01-27. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Hayes, Ian, Nickson, Ray, Strooper, Paul and Colvin, Robert (2000). A Declarative Semantics for Logic Program Refinement. Technical Report no. 00-30. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Colvin, Rob, Hayes, Ian and Strooper, Paul (1999). Refining logic programs using types and invariants. SVRC Technical Report, 99-25. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland.

Hayes, Ian, Fidge, Colin and Lermer, Karl (1999). Semantic identification of dead control-flow paths. SVRC Technical Report, 99-32. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland.

Fidge, C. J., Hayes, I. J., Mahony, B. P. and Wabenhorst, A. K. (1999). Real-time specification and reasoning using maximal intervals. SVRC Technical Report, 99-29. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Smith, Graeme and Hayes, Ian (1999). Towards real-time object-Z. Technical Report SSE, 99-10. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Fidge, Colin. J., Hayes, Ian. J. and Mahony, B. P. (1998). Defining Differentiation and Integration in Z. SVRC Technical Report, 98-09. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Carrington, D., Hayes, I., Nickson, R., Watson, G. N. and Welsh, J. (1996). A Tool for Developing Correct Programs by Refinement. technical Report no. 95-49. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Hayes, I. J. (2002). Block-structured (attribute) grammars. Brisbane, Australia: The University of Queensland.

Hayes, Ian J. and Utting, Mark (1998). Deadlines are termination. Technical Report 98-01 St Lucia, QLD, Australia: Software Verification Research Centre, School of Information Technology, The University of Queensland.

Emeritus Professor Ian Hayes

Researcher biography

Publications

Book Chapters

Journal Articles

Conference Papers

Data Collection

Department Technical Reports

Research Reports