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)

101 - 120 of 151 works

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. TPHOLs: International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, UK, 3–6 September 2001 . Berlin, Heidelberg: Springer Berlin Heidelberg. doi: 10.1007/3-540-44755-5_18

Refinement Calculus for Logic Programming in Isabelle/HOL

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

2000

Conference Publication

Real-time program refinement using auxiliary variables

Hayes, I. J. (2000). Real-time program refinement using auxiliary variables. Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, Pune, India, 20-22 September 2000. Berlin, Germany: Springer. doi: 10.1007/3-540-45352-0_15

Real-time program refinement using auxiliary variables

2000

Conference Publication

Reasoning about real-time programs using idle-invariant assertions

Hayes, I. J. (2000). Reasoning about real-time programs using idle-invariant assertions. APSEC 2000, Singapore, 5-8 December 2000. Washington: IEEE Computer Society. doi: 10.1109/APSEC.2000.896678

Reasoning about real-time programs using idle-invariant assertions

2000

Conference Publication

Structuring real-time Object-Z specifications

Smith, G and Hayes, I (2000). Structuring real-time Object-Z specifications. Integrated Formal Methods: Second International Conference, IFM 2000,, Dagstuhl Castle, Germany, November 2000. Berlin, Germany: Springer. doi: 10.1007/3-540-40911-4_7

Structuring real-time Object-Z specifications

2000

Conference Publication

Refining logic programs using types

Colvin, Robert, Hayes, Ian J. and Strooper, Paul A. (2000). Refining logic programs using types. ACSC 2000, Canberra, ACT, Australia, 31 January - 3 February, 2000. Los Alamitos, CA, USA: IEEE Computer Society. doi: 10.1109/ACSC.2000.824379

Refining logic programs using types

2000

Conference Publication

Reasoning about non-terminating loops using deadline commands

Hayes, I. J. (2000). Reasoning about non-terminating loops using deadline commands. MPC 2000, Ponte de Lima, Portugal, 3-5 July 2000. Berlin: Springer. doi: 10.1007/10722010_5

Reasoning about non-terminating loops using deadline commands

1999

Book

Refining logic programs using types and invariants

Colvin, Rob, Hayes, Ian and Strooper, Paul (1999). Refining logic programs using types and invariants. SVRC Technical Report, 99-25. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland.

Refining logic programs using types and invariants

1999

Book

Semantic identification of dead control-flow paths

Hayes, Ian, Fidge, Colin and Lermer, Karl (1999). Semantic identification of dead control-flow paths. SVRC Technical Report, 99-32. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland.

Semantic identification of dead control-flow paths

1999

Book

Real-time specification and reasoning using maximal intervals

Fidge, C. J., Hayes, I. J., Mahony, B. P. and Wabenhorst, A. K. (1999). Real-time specification and reasoning using maximal intervals. SVRC Technical Report, 99-29. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Real-time specification and reasoning using maximal intervals

1999

Book

Towards real-time object-Z

Smith, Graeme and Hayes, Ian (1999). Towards real-time object-Z. Technical Report SSE, 99-10. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.

Towards real-time object-Z

1999

Journal Article

The deadline command

Fidge, C. J., Hayes, I. J. and Watson, G. N. (1999). The deadline command. IEE Proceedings - Software, 146 (2), 104-111. doi: 10.1049/ip-sen:19990407

The deadline command

1999

Conference Publication

Real-time specification and reasoning using maximal intervals

Fidge, C. J., Hayes, I. J., Mahony, B. and Wabenhorst, A. K. (1999). Real-time specification and reasoning using maximal intervals. PART '99, Melbourne, Australia, 29 Nov - 1 Dec 1999. Singapore: Springer-Verlag.

Real-time specification and reasoning using maximal intervals

1999

Conference Publication

Towards real-time Object-Z

Smith, G. P. and Hayes, I. J. (1999). Towards real-time Object-Z. Integrated Formal Methods IFM'99, York, UK, 28-29 June 1999. London: Springer-Verlag. doi: 10.1007/978-1-4471-0851-1_4

Towards real-time Object-Z

1999

Book Chapter

Specifications are not (necessarily) executable

Hayes, I. J. and Jones, C. B. (1999). Specifications are not (necessarily) executable. High-integrity system specification and design. (pp. 563-581) edited by J. P. Bowen and M. G. Hinchey. London: Springer.

Specifications are not (necessarily) executable

1998

Book

Defining Differentiation and Integration in Z

Fidge, Colin. J., Hayes, Ian. J. and Mahony, B. P. (1998). Defining Differentiation and Integration in Z. SVRC Technical Report, 98-09. Software Verification Research Centre, School of Information Technology, The University of Queensland.

Defining Differentiation and Integration in Z

1998

Journal Article

Expressive Power of Specification Languages

Hayes, Ian J. (1998). Expressive Power of Specification Languages. Formal Aspects of Computing, 10 (2), 187-192. doi: 10.1007/s001650050010

Expressive Power of Specification Languages

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

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