Overview
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
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
Works
Search Professor Ian Hayes’s works on UQ eSpace
2024
Conference Publication
Restructuring a concurrent refinement algebra
Hayes, Ian J., Meinicke, Larissa A. and Evangelou-Oost, Naso (2024). Restructuring a concurrent refinement algebra. 21st International Conference, RAMiCS 2024, Prague, Czech Republic, 19-22 August 2024. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-68279-7_9
2024
Book Chapter
Reasoning about distributive laws in a concurrent refinement algebra
Meinicke, Larissa A. and Hayes, Ian J. (2024). Reasoning about distributive laws in a concurrent refinement algebra. The practice of formal methods: essays in honour of Cliff Jones, part II. (pp. 1-22) edited by Ana Cavalcanti and James Baxter. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-66673-5_1
2024
Book Chapter
Practical rely/guarantee verification of an efficient lock for seL4 on multicore architectures
Colvin, Robert J., Hayes, Ian J., Heiner, Scott, Höfner, Peter, Meinicke, Larissa and Su, Roger C. (2024). Practical rely/guarantee verification of an efficient lock for seL4 on multicore architectures. The practice of formal methods: essays in honour of Cliff Jones, Part I. (pp. 65-87) edited by Ana Cavalcanti and James Baxter. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-66676-6_4
2023
Conference Publication
Differential testing of a verification framework for compiler optimizations (Case study)
Utting, Mark, Webb, Brae J. and Hayes, Ian J. (2023). Differential testing of a verification framework for compiler optimizations (Case study). IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC Australia, 14-15 May 2023. Piscataway, NJ United States: Institute of Electrical and Electronics Engineers.. doi: 10.1109/formalise58978.2023.00015
2023
Conference Publication
Using cylindric algebra to support local variables in rely/guarantee concurrency
Meinicke, Larissa A. and Hayes, Ian J. (2023). Using cylindric algebra to support local variables in rely/guarantee concurrency. IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC, Australia, 14-15 May 2023. Piscataway, NJ, United States: Institute of Electrical and Electronics Engineers. doi: 10.1109/formalise58978.2023.00019
2023
Conference Publication
Verifying term graph optimizations using Isabelle/HOL
Webb, Brae J., Hayes, Ian J. and Utting, Mark (2023). Verifying term graph optimizations using Isabelle/HOL. 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'23), Boston, MA, United States, 16-17 January 2023. New York, NY, United States: ACM. doi: 10.1145/3573105.3575673
2023
Book Chapter
Trace Models of Concurrent Valuation Algebras
Evangelou-Oost, Naso, Meinicke, Larissa, Bannister, Callum and Hayes, Ian J. (2023). Trace Models of Concurrent Valuation Algebras. Formal Methods and Software Engineering. (pp. 118-136) Singapore: Springer Nature Singapore. doi: 10.1007/978-981-99-7584-6_8
2023
Conference Publication
Verifying compiler optimisations (invited paper)
Hayes, Ian J., Utting, Mark and Webb, Brae J. (2023). Verifying compiler optimisations (invited paper). 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, 21–24 November 2023. Singapore, Singapore: Springer Nature Singapore. doi: 10.1007/978-981-99-7584-6_1
2023
Conference Publication
Contextuality in distributed systems
Evangelou-Oost, Nasos, Bannister, Callum and Hayes, Ian J. (2023). Contextuality in distributed systems. 20th International Conference, RAMiCS 2023, Augsburg, Germany, 3-6 April 2023. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-031-28083-2_4
2023
Book Chapter
Specifying and reasoning about shared-variable concurrency
Hayes, Ian J., Jones, Cliff B. and Meinicke, Larissa A. (2023). Specifying and reasoning about shared-variable concurrency. Theories of programming and formal methods. (pp. 110-135) edited by Jonathan P. Bowen, Qin Li and Qiwen Xu. Cham, Switzerland: Springer Nature Switzerland. doi: 10.1007/978-3-031-40436-8_5
2021
Book Chapter
Software specification
Hayes, Ian J. and King, Steve (2021). Software specification. Theories of programming: the life and works of Tony Hoare. (pp. 251-270) edited by Cliff B. Jones and Jayadev Misra. New York, NY USA: Association for Computing Machinery. doi: 10.1145/3477355.3477367
2021
Journal Article
Convolution algebras: relational convolution, generalised modalities and incidence algebras
Dongol, Brijesh, Hayes, Ian J. and Struth, Georg (2021). Convolution algebras: relational convolution, generalised modalities and incidence algebras. Logical Methods in Computer Science, 17 (1) 13, 1-34. doi: 10.23638/LMCS-17(1:13)2021
2021
Conference Publication
A formal semantics of the GraalVM intermediate representation
Webb, Brae J., Utting, Mark and Hayes, Ian J. (2021). A formal semantics of the GraalVM intermediate representation. 19th International Symposium, ATVA 2021, Gold Coast, QLD Australia, 18-22 October 2021. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-88885-5_8
2019
Journal Article
Deriving specifications of control programs for cyber physical systems
Burns, Alan, Hayes, Ian J. and Jones, Cliff B. (2019). Deriving specifications of control programs for cyber physical systems. The Computer Journal, 63 (5), 774-790. doi: 10.1093/comjnl/bxz019
2019
Conference Publication
Cylindric Kleene Lattices for Program Construction
Dongol, Brijesh, Hayes, Ian, Meinicke, Larissa and Struth, Georg (2019). Cylindric Kleene Lattices for Program Construction. MPC: 13th International Conference on Mathematics of Program Construction, Porto, Portugal, 7–9 October 2019. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-33636-3_8
2019
Conference Publication
Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges
Hayes, Ian J. and Meinicke, Larissa A. (2019). Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges. UTP: 7th International Symposium on Unifying Theories of Programming, Porto, Portugal, 8 October 2019. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-31038-7_9
2018
Journal Article
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
Hayes, Ian J., Meinicke, Larissa A., Winter, Kirsten and Colvin, Robert J. (2018). A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects of Computing, 31 (2), 133-163. doi: 10.1007/s00165-018-0464-4
2018
Conference Publication
Encoding fairness in a synchronous concurrent program algebra
Hayes, Ian J. and Meinicke, Larissa A. (2018). Encoding fairness in a synchronous concurrent program algebra. 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 15-17 July 2018. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-95582-7_13
2018
Conference Publication
Some challenges of specifying concurrent program components
Hayes, Ian J. (2018). Some challenges of specifying concurrent program components. 18th Refinement Workshop, Refine 2018, Oxford, United Kingdom, 18 July 2018. SYDNEY: Open Publishing Association. doi: 10.4204/EPTCS.282.2
2018
Conference Publication
A guide to rely/guarantee thinking
Hayes, Ian J. and Jones, Cliff B. (2018). A guide to rely/guarantee thinking. Third International School, SETSS 2017, Chongqing, China, 17–22 April 2017. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-030-02928-9_1
Funding
Current funding
Supervision
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
-
Doctor Philosophy
Design and verification of concurrent systems
Principal Advisor
Other advisors: Dr Larissa Meinicke
-
Doctor Philosophy
Verifying Compiler Optimisation Passes
Associate Advisor
Other advisors: Associate Professor Mark Utting
-
Doctor Philosophy
Concurrent valuation algebras
Associate Advisor
Other advisors: Dr Larissa Meinicke
Completed supervision
-
2022
Doctor Philosophy
Operational Hazard Analysis and the Safety-Aware Concept Development Method
Principal Advisor
Other advisors: Emeritus Professor Paul Bailes
-
2009
Doctor Philosophy
Progress-based verification and derivation of concurrent programs
Principal Advisor
-
-
2008
Doctor Philosophy
Transformation Rules for Probabilistic Programs: An Algebraic Approach
Principal Advisor
-
2006
Doctor Philosophy
INCREMENTAL COMPILATION IN LANGUAGE-BASED ENVIRONMENTS
Principal Advisor
-
2014
Doctor Philosophy
Controlling the Generation of Multiple Counterexamples in LTL Model Checking
Associate Advisor
-
2012
Master Philosophy
FORMAL PROPERTY PRESERVATION AND TRANSFORMATION IN SOFTWARE EVOLUTION
Associate Advisor
Other advisors: Associate Professor Graeme Smith
-
2004
Doctor Philosophy
Towards an object-oriented refinement calculus
Associate Advisor
-
2002
Doctor Philosophy
DATA REFINEMENT AND DATA TYPES IN THE REFINEMENT CALCULUS FOR LOGIC PROGRAMS
Associate Advisor
Media
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: