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)

61 - 80 of 151 works

2009

Conference Publication

CSP with hierarchical state

Colvin, Robert and Hayes, Ian J. (2009). CSP with hierarchical state. 7th International Conference on Integrated Formal Methods: IFM 2009, Dusseldorf, Germany, 16-19 February 2009. New York , U.S.A: Springer-Verlag. doi: 10.1007/978-3-642-00255-7_9

CSP with hierarchical state

2008

Journal Article

Algebraic reasoning for probabilistic action systems and while-loops

Meinicke, Larissa and Hayes, Ian J. (2008). Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica, 45 (5), 321-382. doi: 10.1007/s00236-008-0073-4

Algebraic reasoning for probabilistic action systems and while-loops

2008

Journal Article

Calculating modules in contextual logic program refinement

Colvin, Robert, Hayes, Ian J. and Strooper, Paul A. (2008). Calculating modules in contextual logic program refinement. Theory and Practice of Logic Programming, 8 (1), 1-31. doi: 10.1017/S1471068407003043

Calculating modules in contextual logic program refinement

2008

Conference Publication

Probabilistic Choice in Refinement Algebra

Meinicke, L. and Hayes, I. J. (2008). Probabilistic Choice in Refinement Algebra. 9th International Conference on Mathematics of Program Construction [MPC], Marseille, France, 15-18 July 2008. Berlin, Heidelberg: Springer Verlag. doi: 10.1007/978-3-540-70594-9_14

Probabilistic Choice in Refinement Algebra

2008

Conference Publication

Towards reasoning about teleo-reactive programs for robust real-time systems

Hayes, I.J. (2008). Towards reasoning about teleo-reactive programs for robust real-time systems. 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems (SERENE '08), Newcastle Upon Tyne, UK, 17-19 Nov 2008. New York , U.S.A.: ACM. doi: 10.1145/1479772.1479789

Towards reasoning about teleo-reactive programs for robust real-time systems

2007

Journal Article

Procedures and parameters in the real-time program refinement calculus

Hayes, I. J. (2007). Procedures and parameters in the real-time program refinement calculus. Science of Computer Programming, 64 (3), 286-311. doi: 10.1016/j.scico.2006.06.002

Procedures and parameters in the real-time program refinement calculus

2007

Book Chapter

Deriving specifications for systems that are connected to the physical world

Jones, C. B., Hayes, I. J. and Jackson, M. A. (2007). Deriving specifications for systems that are connected to the physical world. Formal Methods and Hybrid Real-Time Systems. (pp. 364-390) edited by Jones, C. B., Liu, Z. and Woodcock, J.. Berlin, Germany: Springer-Verlag. doi: 10.1007/978-3-540-75221-9_16

Deriving specifications for systems that are connected to the physical world

2006

Conference Publication

Continuous action system refinement

Meinicke, L. A. and Hayes, I. J. (2006). Continuous action system refinement. 8th International Conference on Mathematics of Program Construction (MPC 2006), Kuressaare, Estonia, 3-5 July 2006. Berlin, Germany: Springer-Verlag. doi: 10.1007/11783596_19

Continuous action system refinement

2006

Conference Publication

Termination of real-time programs: definitely, definitely not, or maybe

Hayes, I. J. (2006). Termination of real-time programs: definitely, definitely not, or maybe. First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, 5 - 7 February, 2006. Heidelberg, Germany: Springer Verlag. doi: 10.1007/11768173_9

Termination of real-time programs: definitely, definitely not, or maybe

2006

Conference Publication

Reasoning algebraically about probabilistic loops

Meinicke, Larissa and Hayes, Ian J. (2006). Reasoning algebraically about probabilistic loops. 8th International Conference on Formal Engineering Methods, Macua, PR China, 1-3 November, 2006. Berlin, Germany: Springer-Verlag. doi: 10.1007/11901433_21

Reasoning algebraically about probabilistic loops

2005

Conference Publication

Integration of generic program analysis tools into a software development environment

Glynn, Erica, Hayes, Ian and MacDonald, Anthony (2005). Integration of generic program analysis tools into a software development environment.

Integration of generic program analysis tools into a software development environment

2005

Conference Publication

A theory for execution-time derivation in real-time programs

Lermer, Karl, Fidge, Colin J. and Hayes, Ian J. (2005). A theory for execution-time derivation in real-time programs. doi: 10.1016/j.tcs.2005.08.003

A theory for execution-time derivation in real-time programs

2005

Journal Article

A theory for execution-time derivation in real-time programs

Lermer, Karl, Fidge, Colin J. and Hayes, Ian J. (2005). A theory for execution-time derivation in real-time programs. Theoretical Computer Science, 346 (1), 3-27. doi: 10.1016/j.tcs.2005.08.003

A theory for execution-time derivation in real-time programs

2005

Conference Publication

Integration of generic program analysis tools into a software development environment

Glynn, Erica, Hayes, Ian and Macdonald, Anthony (2005). Integration of generic program analysis tools into a software development environment. Twenty-Eighth Australasian Conference Computer Science, Newcastle, NSW, 31 Jan - 3 Feb 2005. Sydney: Australian Computer Society.

Integration of generic program analysis tools into a software development environment

2005

Edited Outputs

FM2005: Formal Methods

J. Fitzgerald,, I. J. Hayes and A. Tarlecki eds. (2005). FM2005: Formal Methods. International Symposium of Formal Methods Europe, Newcastle, UK, 18-22 July 2005. Berlin: Springer.

FM2005: Formal Methods

2004

Conference Publication

An environment for building a system out of its requirements

Smith, C., Winter, K., Hayes, I., Dromey, G., Lindsay, P. and Carrington, D. (2004). An environment for building a system out of its requirements. Proceedings - 19th International Conference on Automated Software Engineering, ASE 2004, , , September 20, 2004-September 24, 2004. doi: 10.1109/ASE.2004.1342775

An environment for building a system out of its requirements

2004

Conference Publication

Towards platform-independent real-time systems

Hayes, I. J. (2004). Towards platform-independent real-time systems. The 2004 Australian Software Engineering Conference (ASWEC 2004), Melbourne, Australia, 13-16 April 2004. Los Alamitos, California, U.S.A.: IEEE Computer Society. doi: 10.1109/ASWEC.2004.1290472

Towards platform-independent real-time systems

2004

Book Chapter

Developing logic programs from specifications using stepwise refinement

Colvin, Robert, Groves, Lindsay, Hayes, Ian J., Hemer, David, Nickson, Ray and Strooper, Paul (2004). Developing logic programs from specifications using stepwise refinement. Program Development in Computational Logic. (pp. 66-89) edited by Maurice Bruynooghe and Kunk-Kiu Lau. Berlin: Springer Verlag. doi: 10.1007/978-3-540-25951-0_3

Developing logic programs from specifications using stepwise refinement

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

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