Skip to menu Skip to content Skip to footer
Emeritus Professor Ian Hayes
Emeritus Professor

Ian Hayes

Email: 

Overview

Background

Software Engineering. Ian's research interests are in formal methods for software development.

Errors in a compiler for a programming language can generate errors in the myriad of programs they compile. Our research is looking at verifying optimisation phases of a compiler.

Concurrent programs are difficult to reason about due to the interleaving of execution of concurrent threads leading to an explosion of possible execution sequences. Our research is developing techniques for rely/guarantee reasoning about concurrent programs.

Both the above research strands make use of the Isabelle/HOL theorem prover.

Availability

Emeritus Professor Ian Hayes is:
Available for supervision
Media expert

Qualifications

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

Research interests

  • Reasoning about concurrent programs

  • Verified compiler optimisations

Works

Search Professor Ian Hayes’s works on UQ eSpace

151 works between 1978 and 2024

1 - 20 of 151 works

2024

Book Chapter

Practical rely/guarantee verification of an efficient lock for seL4 on multicore architectures

Colvin, Robert J., Hayes, Ian J., Heiner, Scott, Höfner, Peter, Meinicke, Larissa and Su, Roger C. (2024). Practical rely/guarantee verification of an efficient lock for seL4 on multicore architectures. The practice of formal methods: essays in honour of Cliff Jones, Part I. (pp. 65-87) edited by Ana Cavalcanti and James Baxter. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-66676-6_4

Practical rely/guarantee verification of an efficient lock for seL4 on multicore architectures

2024

Conference Publication

Restructuring a concurrent refinement algebra

Hayes, Ian J., Meinicke, Larissa A. and Evangelou-Oost, Naso (2024). Restructuring a concurrent refinement algebra. 21st International Conference, RAMiCS 2024, Prague, Czech Republic, 19-22 August 2024. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-68279-7_9

Restructuring a concurrent refinement algebra

2024

Book Chapter

Reasoning about distributive laws in a concurrent refinement algebra

Meinicke, Larissa A. and Hayes, Ian J. (2024). Reasoning about distributive laws in a concurrent refinement algebra. The practice of formal methods: essays in honour of Cliff Jones, part II. (pp. 1-22) edited by Ana Cavalcanti and James Baxter. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-66673-5_1

Reasoning about distributive laws in a concurrent refinement algebra

2023

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

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

2023

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

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

2023

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

Verifying term graph optimizations using Isabelle/HOL

2023

Conference Publication

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

Verifying compiler optimisations (invited paper)

2023

Conference Publication

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

Contextuality in distributed systems

2023

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

Specifying and reasoning about shared-variable concurrency

2023

Book Chapter

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

Trace Models of Concurrent Valuation Algebras

2021

Book Chapter

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

Software specification

2021

Journal Article

Convolution algebras: relational convolution, generalised modalities and incidence algebras

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

Convolution algebras: relational convolution, generalised modalities and incidence algebras

2021

Conference Publication

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

A formal semantics of the GraalVM intermediate representation

2019

Journal Article

Deriving specifications of control programs for cyber physical systems

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

Deriving specifications of control programs for cyber physical systems

2019

Conference Publication

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

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

2019

Conference Publication

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

Cylindric Kleene Lattices for Program Construction

2018

Journal Article

A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency

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

A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency

2018

Conference Publication

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

A guide to rely/guarantee thinking

2018

Conference Publication

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

Type capabilities for object-oriented programming languages

2018

Conference Publication

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

Engineering a theory of concurrent programming

Funding

Current funding

  • 2019 - 2026
    Verifying Graal Optimization Passes
    Oracle Labs
    Open grant

Past funding

  • 2021 - 2024
    Verifying Concurrent Data Structures for Multicore seL4 (DSTG grant administered by ANU)
    Australian National University
    Open grant
  • 2019 - 2023
    Design and verification of correct, efficient and secure concurrent systems
    ARC Discovery Projects
    Open grant
  • 2015 - 2019
    An extensible framework for analysis of Java language-based security conformance
    ARC Linkage Projects
    Open grant
  • 2013 - 2015
    Understanding concurrent programs using rely-guarantee thinking
    ARC Discovery Projects
    Open grant
  • 2011 - 2014
    Software Quality Improvement Through Static Analysis and Annotation
    ARC Linkage Projects
    Open grant
  • 2009 - 2012
    Reducing the risks associated with developing large-scale, critical software-integrated systems (ARC Linkage Project administered by Griffith University)
    Griffith University
    Open grant
  • 2009 - 2011
    Combining Time Bands and Teleo-Reactive Programs for Advanced Dependable Real-Time Systems
    ARC Discovery Projects
    Open grant
  • 2005 - 2007
    Analysing and Generating Fault-Tolerant Real-Time Systems
    ARC Discovery Projects
    Open grant
  • 2003 - 2008
    ARC Centre for Complex Systems
    ARC Centres of Excellence
    Open grant
  • 2003
    Building dependability into complex, computer-based systems
    ARC Discovery Projects
    Open grant
  • 2002 - 2003
    Derivation and timing analysis of concurrent real-time software
    ARC Discovery Projects
    Open grant
  • 2002
    Using decomposition and abstraction to support automatic reasoning about complex combined software and hardware systems.
    UQ External Support Enabling Grant
    Open grant
  • 2001
    A tool for reasoning about combined hardware and software systems.
    University of Queensland Small Grants Scheme
    Open grant
  • 1999 - 2001
    Effective Real-Time Program Analysis
    ARC Australian Research Council (Large grants)
    Open grant
  • 1999 - 2001
    Refinement Calculus for Logic Programming
    ARC Australian Research Council (Large grants)
    Open grant
  • 1998 - 2000
    A unified formalism for concurrent real time software development
    ARC Australian Research Council (Large grants)
    Open grant
  • 1997
    Refinement Calculus for Logic Programming
    UQ External Support Enabling Grant
    Open grant
  • 1997
    Timing path analysis of high-level real-time programs
    ARC Australian Research Council (Small grants)
    Open grant
  • 1996
    Adding flexible modularisation to the refinement calculus
    UQ External Support Enabling Grant
    Open grant
  • 1996
    Refinement calculus for logic programming
    ARC Australian Research Council (Small grants)
    Open grant
  • 1995
    Specification and refinement of real time control systems
    UQ External Support Enabling Grant
    Open grant

Supervision

Availability

Emeritus Professor Ian Hayes is:
Available for supervision

Before you email them, read our advice on how to contact a supervisor.

Supervision history

Current supervision

Completed supervision

Media

Enquiries

Contact Emeritus Professor Ian Hayes directly for media enquiries about:

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

Need help?

For help with finding experts, story ideas and media enquiries, contact our Media team:

communications@uq.edu.au