OR

Browse By

Emeritus Professor Ian Hayes

Emeritus Professor

School of Electrical Engineering and Computer Science
Faculty of Engineering, Architecture and Information Technology
ian.hayes@uq.edu.au

Overview

Software Engineering. Ian's research interests are in formal methods for software development, particularly for concurrent and real-time systems.

He is currently the head of the Systems and Software Engineering Research Group.

Research Interests

  • Reasoning about concurrent programs
  • Program analysis

Qualifications

  • Doctor of Philosophy, University of New South Wales
  • Bachelor (Honours) of Science (Advanced), University of New South Wales

Publications

  • Conference Publication: Differential testing of a verification framework for compiler optimizations (Case study)

    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

  • Conference Publication: Using cylindric algebra to support local variables in rely/guarantee concurrency

    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

  • Conference Publication: Verifying term graph optimizations using Isabelle/HOL

    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

View all Publications

Grants

View all Grants

Supervision

View all Supervision

Publications

Book

  • Refining logic programs using types and invariants

    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.

  • Semantic identification of dead control-flow paths

    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.

  • Real-time specification and reasoning using maximal intervals

    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.

  • Towards real-time object-Z

    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.

  • Defining Differentiation and Integration in Z

    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.

Book Chapter

  • Specifying and reasoning about shared-variable concurrency

    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

  • Trace Models of Concurrent Valuation Algebras

    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

  • Software specification

    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

  • Dynamically detecting faults via integrity constraints

    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

  • Deriving specifications for systems that are connected to the physical world

    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

  • Developing logic programs from specifications using stepwise refinement

    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

  • A predicative semantics for real-time refinement

    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

  • Specifications are not (necessarily) executable

    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.

  • Deadlines are termination

    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

Journal Article

Conference Publication

  • Differential testing of a verification framework for compiler optimizations (Case study)

    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

  • Using cylindric algebra to support local variables in rely/guarantee concurrency

    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

  • Verifying term graph optimizations using Isabelle/HOL

    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

  • Contextuality in distributed systems

    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

  • Verifying compiler optimisations (invited paper)

    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

  • A formal semantics of the GraalVM intermediate representation

    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

  • Cylindric Kleene Lattices for Program Construction

    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

  • Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges

    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

  • A guide to rely/guarantee thinking

    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

  • Encoding fairness in a synchronous concurrent program algebra

    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

  • Engineering a theory of concurrent programming

    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

  • Some challenges of specifying concurrent program components

    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

  • Type capabilities for object-oriented programming languages

    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

  • Capabilities for Java: Secure access to resources

    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

  • An algebra of synchronous atomic steps

    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

  • Separating concerns of rely and guarantee in concurrent program derivation

    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

  • Invariants, well-founded statements and real-time program algebra

    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

  • Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions

    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

  • Path-sensitive data flow analysis simplified

    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

  • Visuocode: A software development environment that supports spatial navigation and composition

    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

  • Deriving real-time action systems controllers from multiscale system specifications

    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

  • Fractional permissions and non-deterministic evaluators in interval temporal logic

    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

  • Integrated operational semantics: small-step, big-step and multi-step

    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

  • Model-driven web form validation with UML and OCL

    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

  • Rely/guarantee reasoning for teleo-reactive programs over multiple time bands

    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

  • Towards an algebra for real-time programs

    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

  • Approximating idealised real-time specifications using time bands

    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

  • Compositional action system derivation using enforced properties

    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

  • Integrating requirements: The behavior tree philosophy

    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

  • Invariants and well-foundedness in program algebra

    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

  • Reasoning about loops in total and general correctness

    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

  • Unifying theories of programming that distinguish nontermination and abort

    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

  • Dynamically detecting faults via integrity constraints

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

  • CSP with hierarchical state

    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

  • Enforcing safety and progress properties: An approach to concurrent program derivation

    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

  • Probabilistic Choice in Refinement Algebra

    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

  • Towards reasoning about teleo-reactive programs for robust real-time systems

    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

  • Continuous action system refinement

    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

  • Reasoning algebraically about probabilistic loops

    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

  • Termination of real-time programs: definitely, definitely not, or maybe

    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

  • Integration of generic program analysis tools into a software development environment

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

  • A theory for execution-time derivation in real-time programs

    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

  • Integration of generic program analysis tools into a software development environment

    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.

  • An environment for building a system out of its requirements

    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

  • Towards platform-independent real-time systems

    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

  • Determining the specification of a control system from that of its environment

    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

  • Formal Semantics for Program Paths

    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

  • Programs as paths: An approach to timing constraint analysis

    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

  • Reasoning about deadlines in concurrent real-time programs

    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

  • Refinement of higher-order logic programs

    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

  • Reasoning about real-time repetitions: Terminating and nonterminating

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

  • An introduction to real-time Object-Z

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

  • Don't care non-determinism in logic program refinement

    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

  • Reasoning about timeouts

    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

  • Refining object-orientated invariants and dynamic constraints

    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.

  • The real-time refinement calculus: A foundation for machine-independent real-time programming

    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

  • Towards a refinement calculus for concurrent real-time programs

    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

  • Translating refined logic programs to Mercury

    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..

  • A technique for modular logic program refinement

    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

  • Refinement Calculus for Logic Programming in Isabelle/HOL

    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

  • Refinement calculus for logic programming in Isabelle/HOL

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

  • Using theory interpretation to mechanise the reals in a theorem prover

    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

  • Using theory interpretation to mechanise the reals in a theorem prover

    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.

  • Real-time program refinement using auxiliary variables

    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

  • Reasoning about non-terminating loops using deadline commands

    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

  • Reasoning about real-time programs using idle-invariant assertions

    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

  • Refining logic programs using types

    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

  • Structuring real-time Object-Z specifications

    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

  • Real-time specification and reasoning using maximal intervals

    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.

  • Towards real-time Object-Z

    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

  • A set-theoretic model for real-time specification and reasoning

    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

  • Data refining logic programs

    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.

  • Defining differentiation and integration in Z

    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

  • A tool for logic program refinement (Extended abstract)

    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..

  • Coercing real-time refinement: a transmitter

    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

  • Integrating real-time scheduling theory and program refinement

    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

  • Refining specifications to logic programs

    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

  • A formal semantics for a language with type extension

    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.

  • Are formal methods relevant?

    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

  • Communicating technologist: an educational challenge

    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

  • Deriving modular designs from formal specifications

    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

  • Towards Libraries for Z

    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

  • A Case Study in Timed Refinement: A Central Heater

    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

  • Interpretations of Z Schema Operators

    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

  • A Generalisation of Bags in Z

    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

  • Using mathematics to specify software

    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.

Edited Outputs

  • FM2005: Formal Methods

    J. Fitzgerald,, I. J. Hayes and A. Tarlecki eds. (2005). FM2005: Formal Methods. International Symposium of Formal Methods Europe, Newcastle, UK, 18-22 July 2005. Berlin: Springer.

Other Outputs

  • Prolog

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

  • Reasoning about teleo-reactive programs under parallel composition

    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.

  • Block-structured (attribute) grammars

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

  • Deadlines are termination

    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.

Grants (Administered at UQ)

PhD and MPhil Supervision

Current Supervision

  • Design and verification of concurrent systems

    Doctor Philosophy — Principal Advisor

    Other advisors:

  • Verifying Compiler Optimisation Passes

    Doctor Philosophy — Associate Advisor

    Other advisors:

Completed Supervision

This staff member is a UQ Expert for media in the following fields:

Software development, Computer software development, Software engineering, Engineering - software, Real-time systems - IT

They are happy to lend their expertise to your articles or broadcasts and share their research discoveries and insights with the community via media channels.

For additional assistance with story ideas, general advice and information or help with seeking further experts, please email the UQ Media Team or telephone (07) 3365 1120.

Links

ORCID: 0000-0003-3649-392X

Scopus ID: 7004615706

Personal Profile: Link

Unit Links
Other Media

Related Resources

Similar Staff
Researchers in Associated Units
Fields of Research