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)

121 - 140 of 151 works

1998

Journal Article

A Program Refinement Tool

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

A Program Refinement Tool

1998

Conference Publication

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.

Data refining logic programs

1998

Conference Publication

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

Defining differentiation and integration in Z

1998

Book Chapter

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

Deadlines are termination

1998

Other Outputs

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.

Deadlines are termination

1997

Journal Article

Supporting contexts in program refinement

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

Supporting contexts in program refinement

1997

Conference Publication

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

A tool for logic program refinement (Extended abstract)

1996

Conference Publication

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

Refining specifications to logic programs

1996

Conference Publication

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

Integrating real-time scheduling theory and program refinement

1996

Journal Article

Supporting module reuse in refinement

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

Supporting module reuse in refinement

1996

Conference Publication

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

Coercing real-time refinement: a transmitter

1995

Journal Article

Specification by interface separation

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

Specification by interface separation

1995

Journal Article

Using units of measurement in formal specifications

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

Using units of measurement in formal specifications

1995

Conference Publication

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

Communicating technologist: an educational challenge

1995

Conference Publication

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

Are formal methods relevant?

1995

Conference Publication

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.

A formal semantics for a language with type extension

1993

Conference Publication

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

Towards Libraries for Z

1993

Conference Publication

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

Deriving modular designs from formal specifications

1992

Journal Article

A case-study in timed refinement: A mine pump

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

A case-study in timed refinement: A mine pump

1992

Journal Article

VDM and Z: A comparative case study

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

VDM and Z: A comparative case study

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