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)

81 - 100 of 151 works

2003

Conference Publication

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

Refinement of higher-order logic programs

2003

Conference Publication

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

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

2003

Conference Publication

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

Formal Semantics for Program Paths

2003

Book Chapter

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

A predicative semantics for real-time refinement

2003

Conference Publication

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

Programs as paths: An approach to timing constraint analysis

2002

Conference Publication

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

Reasoning about real-time repetitions: Terminating and nonterminating

2002

Conference Publication

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

Reasoning about timeouts

2002

Conference Publication

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

An introduction to real-time Object-Z

2002

Journal Article

Refining object-oriented invariants and dynamic constraints

Shield, J. and Hayes, I. J. (2002). Refining object-oriented invariants and dynamic constraints. Proceedings - Asia-Pacific Software Engineering Conference, APSEC 1182975, 52-61. doi: 10.1109/APSEC.2002.1182975

Refining object-oriented invariants and dynamic constraints

2002

Conference Publication

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

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

2002

Conference Publication

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

Towards a refinement calculus for concurrent real-time programs

2002

Other Outputs

Block-structured (attribute) grammars

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

Block-structured (attribute) grammars

2002

Journal Article

Reasoning about real-time repetitions: terminating and nonterminating

Hayes, Ian (2002). Reasoning about real-time repetitions: terminating and nonterminating. Science of Computer Programming, 43 (2-3), 161-192. doi: 10.1016/S0167-6423(02)00024-2

Reasoning about real-time repetitions: terminating and nonterminating

2002

Conference Publication

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.

Refining object-orientated invariants and dynamic constraints

2002

Journal Article

A refinement calculus for logic programs

Hayes, Ian, Colvin, Robert, Hemer, David, Strooper, Paul and Nickson, Ray (2002). A refinement calculus for logic programs. Theory And Practice of Logic Programming, 2 (Part 4-5), 425-460. doi: 10.1017/S1471068402001448

A refinement calculus for logic programs

2002

Conference Publication

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

Don't care non-determinism in logic program refinement

2002

Conference Publication

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

Translating refined logic programs to Mercury

2001

Conference Publication

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

A technique for modular logic program refinement

2001

Journal Article

Semantic characterisation of dead control-flow paths

Hayes, I. J., Fidge, C. J. and Lermer, K. R. C. (2001). Semantic characterisation of dead control-flow paths. IEE Proceedings Software, 148 (6), 175-186. doi: 10.1049/ip-sen:20010834

Semantic characterisation of dead control-flow paths

2001

Conference Publication

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.

Refinement calculus for logic programming in Isabelle/HOL

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