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
2012
Journal Article
Preface: Morgan: a suitable case for treatment
Höfner, Peter, Van Glabbeek, Rob and Hayes, Ian (2012). Preface: Morgan: a suitable case for treatment. Formal Aspects of Computing, 24 (4-6), 417-422. doi: 10.1007/s00165-012-0257-0
2012
Conference Publication
Integrated operational semantics: small-step, big-step and multi-step
Hayes, Ian J. and Colvin, Robert J. (2012). Integrated operational semantics: small-step, big-step and multi-step. 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), Pisa, Italy, 18-21 June 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-30885-7_2
2012
Conference Publication
Towards an algebra for real-time programs
Dongol, Brijesh, Hayes, Ian J., Meinicke, Larissa and Solin, Kim (2012). Towards an algebra for real-time programs. 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012), Cambridge, United Kingdom, 17 - 20 September 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-33314-9_4
2012
Conference Publication
Deriving real-time action systems controllers from multiscale system specifications
Dongol, Brijesh and Hayes, Ian J. (2012). Deriving real-time action systems controllers from multiscale system specifications. Mathematics of Program Construction 11th International Conference, MPC 2012, Madrid, Spain, 25 - 27 June 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-31113-0_7
2012
Conference Publication
Model-driven web form validation with UML and OCL
Escott, Eban, Strooper, Paul, King, Paul and Hayes, Ian J. (2012). Model-driven web form validation with UML and OCL. 11th International Conference on Web Engineering (ICWE 2011), Paphos, Cyprus, 20-21 June 2011. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-27997-3_23
2012
Conference Publication
Rely/guarantee reasoning for teleo-reactive programs over multiple time bands
Dongol, Brijesh and Hayes, Ian J. (2012). Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. 9th International Conference on Integrated Formal Methods (IFM 2012), Pisa, Italy, 18-21 June 2012. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-30729-4_4
2012
Conference Publication
Fractional permissions and non-deterministic evaluators in interval temporal logic
Dongol, Brijesh, Derrick, John and Hayes, Ian J. (2012). Fractional permissions and non-deterministic evaluators in interval temporal logic. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Bamberg, Germany, 18–20 September 2012. Berlin, Germany: European Association of Software Science and Technology (E A S S T). doi: 10.14279/tuj.eceasst.53.792.791
2011
Journal Article
A semantics for Behavior Trees using CSP with specification commands
Colvin, Robert J. and Hayes, Ian J. (2011). A semantics for Behavior Trees using CSP with specification commands. Science of Computer Programming, 76 (10), 891-914. doi: 10.1016/j.scico.2010.11.007
2011
Journal Article
Structural operational semantics through context-dependent behaviour
Colvin, Robert J. and Hayes, Ian J. (2011). Structural operational semantics through context-dependent behaviour. Journal of Logic and Algebraic Programming, 80 (7), 392-426. doi: 10.1016/j.jlap.2011.05.001
2011
Other Outputs
Reasoning about teleo-reactive programs under parallel composition
Dongol, Brijesh and Hayes, Ian J. (2011). Reasoning about teleo-reactive programs under parallel composition. Technical Report SSE, 2011-01. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
2011
Conference Publication
Approximating idealised real-time specifications using time bands
Dongol, Brijesh and Hayes, Ian J. (2011). Approximating idealised real-time specifications using time bands. 11th International Workshop on Automated Verification of Critical Systems, Newcastle upon Tyne, United Kingdom, 12-14 September 2011. Berlin, Germany: European Association of Software Science and Technology. doi: 10.14279/tuj.eceasst.46.684.701
2010
Journal Article
A timeband framework for modelling real-time systems
Burns, Alan and Hayes, Ian J. (2010). A timeband framework for modelling real-time systems. Real-time Systems [computer resource], 45 (1-2), 106-142. doi: 10.1007/s11241-010-9094-5
2010
Conference Publication
Compositional action system derivation using enforced properties
Dongol, Brijesh and Hayes, Ian J. (2010). Compositional action system derivation using enforced properties. Mathematics of Program Construction [MPC], Quebec City, Quebec, Canada, 21-23 June, 2010. Berlin, Germany: Springer. doi: 10.1007/978-3-642-13321-3_9
2010
Conference Publication
Integrating requirements: The behavior tree philosophy
Winter, Kirsten, Hayes, Ian J. and Colvin, Robert (2010). Integrating requirements: The behavior tree philosophy. Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, 13-18 September 2010. United States: IEEE Computer Society. doi: 10.1109/SEFM.2010.13
2010
Conference Publication
Invariants and well-foundedness in program algebra
Hayes, Ian J. (2010). Invariants and well-foundedness in program algebra. 7th International Colloquium on Theoretical Aspects of Computing (ICTAC 2010), Natal, Rio Grande do Norte, Brazil, 1-3 September 2010. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-14808-8_1
2010
Conference Publication
Unifying theories of programming that distinguish nontermination and abort
Hayes, I. J., Dunne, S. E. and Meinicke, L. (2010). Unifying theories of programming that distinguish nontermination and abort. Mathematics of Program Construction [MPC], Québec City, Québec, Canada, 21-23 June, 2010. Berlin, Germany: Springer. doi: 10.1007/978-3-642-13321-3
2010
Conference Publication
Reasoning about loops in total and general correctness
Dunne, Steve E., Hayes, Ian J. and Galloway, Andy J. (2010). Reasoning about loops in total and general correctness. Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, 8-10 September, 2008. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-14521-6_5
2009
Conference Publication
Dynamically detecting faults via integrity constraints
Hayes, Ian J. (2009). Dynamically detecting faults via integrity constraints. doi: 10.1007/978-3-642-00867-2_5
2009
Conference Publication
Enforcing safety and progress properties: An approach to concurrent program derivation
Dongol, Brijesh and Hayes, Ian J. (2009). Enforcing safety and progress properties: An approach to concurrent program derivation. Australian Software Engineering Conference [ASWEC], Gold Coast , Australia, 14-17 April 2009. Los Alamitos, CA, U.S.A.: IEEE Computer Society. doi: 10.1109/ASWEC.2009.12
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
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 GraalVM Compiler Optimizations
Associate Advisor
Other advisors: Associate Professor Mark Utting
-
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
-
Doctor Philosophy
A hybrid model for a concurrent refinement algebra
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: