Emeritus Professor Ian Hayes
Emeritus Professor

Ian Hayes

Email: 

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

Fields of research

Information and Computing Sciences

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

Search Professor Ian Hayes’s works on UQ eSpace

151 works between 1978 and 2024
All (151) Journal Article (43) Book Chapter (11) Conference Publication (87) Book (5) Other Outputs (4) Edited Outputs (1)

141 - 151 of 151 works

1992

Journal Article

Multi-relations in Z: A cross between multi-sets and binary relations

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

Multi-relations in Z: A cross between multi-sets and binary relations

1991

Journal Article

Case studies in systematic software development

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

Case studies in systematic software development

1991

Journal Article

The semantics of programming languages: An elementary introduction using structural operational semantics

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

The semantics of programming languages: An elementary introduction using structural operational semantics

1991

Conference Publication

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

A Case Study in Timed Refinement: A Central Heater

1991

Conference Publication

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

Interpretations of Z Schema Operators

1990

Conference Publication

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

A Generalisation of Bags in Z

1987

Journal Article

Laws of programming

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

Laws of programming

1986

Journal Article

Specification directed module testing

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

Specification directed module testing

1986

Conference Publication

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.

Using mathematics to specify software

1985

Journal Article

APPLYING FORMAL SPECIFICATION TO SOFTWARE DEVELOPMENT IN INDUSTRY

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

APPLYING FORMAL SPECIFICATION TO SOFTWARE DEVELOPMENT IN INDUSTRY

1978

Journal Article

Some remarks on "Ambiguous Machine Architecture"

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

Some remarks on "Ambiguous Machine Architecture"

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

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

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