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)

21 - 40 of 151 works

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

2017

Journal Article

Designing a semantic model for a wide-spectrum language with concurrency

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

Designing a semantic model for a wide-spectrum language with concurrency

2017

Conference Publication

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

Capabilities for Java: Secure access to resources

2016

Journal Article

Possible values: exploring a concept for concurrency

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

Possible values: exploring a concept for concurrency

2016

Journal Article

Generalised rely-guarantee concurrency: an algebraic foundation

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

Generalised rely-guarantee concurrency: an algebraic foundation

2016

Journal Article

Convolution as a unifying concept: applications in separation logic, interval calculi, and concurrency

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

Convolution as a unifying concept: applications in separation logic, interval calculi, and concurrency

2016

Conference Publication

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

An algebra of synchronous atomic steps

2015

Conference Publication

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

Separating concerns of rely and guarantee in concurrent program derivation

2014

Journal Article

Balancing expressiveness in formal approaches to concurrency

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

Balancing expressiveness in formal approaches to concurrency

2014

Journal Article

Deriving real-time action systems with multiple time bands using algebraic reasoning

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

Deriving real-time action systems with multiple time bands using algebraic reasoning

2014

Journal Article

Reasoning about goal-directed real-time teleo-reactive programs

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

Reasoning about goal-directed real-time teleo-reactive programs

2014

Conference Publication

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

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

2014

Conference Publication

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

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

2013

Journal Article

Linking unifying theories of program refinement

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

Linking unifying theories of program refinement

2013

Journal Article

Deriving real-time action systems in a sampling logic

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

Deriving real-time action systems in a sampling logic

2013

Journal Article

Comparing degrees of non-Determinism in expression evaluation

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

Comparing degrees of non-Determinism in expression evaluation

2013

Conference Publication

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

Path-sensitive data flow analysis simplified

2013

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

Prolog

2013

Conference Publication

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

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

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