Emeritus Professor Ian Hayes
Emeritus Professor
School of Electrical Engineering and Computer Science
Researcher biography
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.
| Featured projects | Duration |
|---|---|
|
Design and verification of correct, efficient and secure concurrent systems ARC Discovery Project |
2019–2022 |
| Verifying GraalVM Optimization Passes | 2020–2026 |
Publications
Book Chapters
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
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
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
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
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
Hayes, Ian J. (2009). Dynamically detecting faults via integrity constraints. Methods, Models, and Tools for Fault Tolerance. (pp. 85-103) edited by Michael Butler, Cliff Jones, Alexander Romanovsky and Elena Troubitsyna. Berlin, Germany: Springer Verlag. doi: 10.1007/978-3-642-00867-2_5
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
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
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
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.
Hayes, I. J. and Utting, M. (1998). Deadlines are termination. Programming Concepts and Methods PROCOMET ’98. (pp. 186-204) Boston, MA, United States: Springer. doi: 10.1007/978-0-387-35358-6_15
Journal Articles
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
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
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
Colvin, Robert J., Hayes, Ian J. and Meinicke, Larissa A. (2017). Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects of Computing, 29 (5), 1-23. doi: 10.1007/s00165-017-0416-4
Jones, Cliff B. and Hayes, Ian J. (2016). Possible values: exploring a concept for concurrency. Journal of Logical and Algebraic Methods in Programming, 85 (5 Part 2), 972-984. doi: 10.1016/j.jlamp.2016.01.002
Hayes, Ian J. (2016). Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects of Computing, 28 (6), 1057-1078. doi: 10.1007/s00165-016-0384-0
Dongol, Brijesh, Hayes, Ian J. and Struth, Georg (2016). Convolution as a unifying concept: applications in separation logic, interval calculi, and concurrency. ACM Transactions on Computational Logic, 17 (3) 15, 1-25. doi: 10.1145/2874773
Jones, Cliff B., Hayes, Ian J. and Colvin, Robert J. (2014). Balancing expressiveness in formal approaches to concurrency. Formal Aspects of Computing, 27 (3), 1-23. doi: 10.1007/s00165-014-0310-2
Dongol, Brijesh, Hayes, Ian J. and Derrick, John (2014). Deriving real-time action systems with multiple time bands using algebraic reasoning. Science of Computer Programming, 85 (PART B), 137-165. doi: 10.1016/j.scico.2013.08.009
Dongol, Brijesh, Hayes, Ian J. and Robinson, Peter J. (2014). Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects of Computing, 26 (3), 563-589. doi: 10.1007/s00165-012-0272-1
Dongol, Brijesh and Hayes, Ian J. (2013). Deriving real-time action systems in a sampling logic. Science of Computer Programming, 78 (11), 2047-2063. doi: 10.1016/j.scico.2012.07.008
Hayes, Ian J., Dunne, Steve E. and Meinicke, Larissa A. (2013). Linking unifying theories of program refinement. Science of Computer Programming, 78 (11), 2086-2107. doi: 10.1016/j.scico.2012.07.010
Hayes, Ian J., Burns, Alan, Dongol, Brijesh and Jones, Cliff B. (2013). Comparing degrees of non-Determinism in expression evaluation. Computer Journal, 56 (6), 741-755. doi: 10.1093/comjnl/bxt005
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
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
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
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
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
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
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
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
Lermer, K. R. C., Fidge, C. J. and Hayes, I. J. (2003). Linear approximation of execution-time constraints. Formal Aspects of Computing, 15 (4), 319-348. doi: 10.1007/s00165-003-0019-0
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
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
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
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
Hayes, I. J. and Utting, M. (2001). A sequential real-time refinement calculus. Acta Informatica, 37 (6), 385-448. doi: 10.1007/PL00013311
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
Hayes, Ian J. (1998). Expressive Power of Specification Languages. Formal Aspects of Computing, 10 (2), 187-192. doi: 10.1007/s001650050010
Carrington D., Hayes I., Nickson R., Watson G. and Welsh J. (1998). A Program Refinement Tool. Formal Aspects of Computing, 10 (2), 97-124. doi: 10.1007/s001650050006
Nickson, R and Hayes, I (1997). Supporting contexts in program refinement. Science of Computer Programming, 29 (3), 279-302. doi: 10.1016/S0167-6423(97)00002-6
Hayes I.J. (1996). Supporting module reuse in refinement. Science of Computer Programming, 27 (2), 175-184. doi: 10.1016/0167-6423(96)00006-8
Hayes, I. J. and Sanders, J. W. (1995). Specification by interface separation. Formal Aspects of Computing, 7 (4), 430-439. doi: 10.1007/bf01211217
Hayes, Ian J. and Mahony, Brendan P. (1995). Using units of measurement in formal specifications. Formal Aspects of Computing, 7 (3), 329-347. doi: 10.1007/bf01211077
Mahony B.P. and Hayes I.J. (1992). A case-study in timed refinement: A mine pump. IEEE Transactions on Software Engineering, 18 (9), 817-826. doi: 10.1109/32.159841
Hayes, Ian (1992). Multi-relations in Z: A cross between multi-sets and binary relations. Acta Informatica, 29 (1), 33-62. doi: 10.1007/BF01178565
Hayes, Ian (1992). VDM and Z: A comparative case study. Formal Aspects of Computing, 4 (1), 76-99. doi: 10.1007/bf01214957
Hayes, Ian J. (1991). Case studies in systematic software development. Science of Computer Programming, 17 (1-3), 250-251. doi: 10.1016/0167-6423(91)90042-v
Hayes, Ian J. (1991). The semantics of programming languages: An elementary introduction using structural operational semantics. Science of Computer Programming, 16 (3), 278-279. doi: 10.1016/0167-6423(91)90011-l
Hoare, C. A.R., Hayes, I. J., Jifeng, He, Morgan, C. C., Roscoe, A. W., Sanders, J. W., Sorensen, I. H., Spivey, J. M. and Sufrin, B. A. (1987). Laws of programming. Communications of the ACM, 30 (8), 672-686. doi: 10.1145/27651.27653
Hayes, Ian J. (1986). Specification directed module testing. IEEE Transactions on Software Engineering, SE-12 (1), 124-133. doi: 10.1109/tse.1986.6312926
Hayes, Ian J. (1985). APPLYING FORMAL SPECIFICATION TO SOFTWARE DEVELOPMENT IN INDUSTRY. IEEE Transactions on Software Engineering, SE-11 (2), 169-178. doi: 10.1109/TSE.1985.232191
Hayes, Ian J. (1978). Some remarks on "Ambiguous Machine Architecture". ACM SIGARCH Computer Architecture News, 6 (8), 23-24. doi: 10.1145/1216467.1216473
Conference Papers
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
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
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
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
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
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
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
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
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
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
Hayes, Ian J. (2018). Engineering a theory of concurrent programming. 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, 12-16 November 2018. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-02450-5_1
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
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
Wu, Xi, Lu, Yi, Meiring, Patrick A., Hayes, Ian J. and Meinicke, Larissa A. (2018). Type capabilities for object-oriented programming languages. 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD Australia, 12-16 November 2018. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-02450-5_13
Hayes, Ian J., Wu, Xi and Meinicke, Larissa A. (2017). Capabilities for Java: Secure access to resources. 15th Asian Symposium on Programming Languages and Systems, APLAS 2017, Suzhou, People's Republic of China, 27-29 November 2017. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-71237-6_4
Hayes, Ian J., Colvin, Robert J., Meinicke, Larissa A., Winter, Kirsten and Velykis, Andrius (2016). An algebra of synchronous atomic steps. 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, 9-11 November 2016. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-48989-6_22
Hayes, Ian J. (2015). Separating concerns of rely and guarantee in concurrent program derivation. Unifying Theories of Programming: 5th International Symposium, Singapore, 13 May, 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-14806-9
Hayes, Ian J. (2014). Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions. 2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013, Queenstown, 29 - 30 October 2013. Springer Verlag. doi: 10.1007/978-3-319-05416-2_1
Hayes, Ian J. and Meinicke, Larissa (2014). Invariants, well-founded statements and real-time program algebra. 19th International Symposium on Formal Methods, FM 2014, Singapore, 12 - 16 May 2014. Heidelberg, Germany: Springer Verlag. doi: 10.1007/978-3-319-06410-9_23
Bradley, Daniel R. and Hayes, Ian J. (2013). Visuocode: A software development environment that supports spatial navigation and composition. 1st IEEE Working Conference on Software Visualization, VISSOFT 2013, Eindhoven, The Netherlands, 27 - 28 September 2013. Piscatawa, NJ United States: I E E E. doi: 10.1109/VISSOFT.2013.6650533
Winter, Kirsten, Zhang, Chenyi, Hayes, Ian J., Keynes, Nathan, Cifuentes, Cristina and Li, Lisa (2013). Path-sensitive data flow analysis simplified. 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, 29 October - 1 November 2013. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-41202-8_27
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
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
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
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
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
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
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
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
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
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
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
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
Hayes, Ian J. (2009). Dynamically detecting faults via integrity constraints. doi: 10.1007/978-3-642-00867-2_5
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
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
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
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
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
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
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
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
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.
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
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
Peuker, S. and Hayes, I. J. (2003). Reasoning about deadlines in concurrent real-time programs. International Parallel and Distributed Processing Symposium 2003, Nice, France, 22-26 April 2003. Los Alamitos, CA, U.S.A.: IEEE Computer Society. doi: 10.1109/IPDPS.2003.1213430
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
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
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
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
Hayes, Ian (2002). Reasoning about real-time repetitions: Terminating and nonterminating. doi: 10.1016/S0167-6423(02)00024-2
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
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..
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
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.
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
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
Smith, G. P. and Hayes, I. J. (2002). An introduction to real-time Object-Z. London: Springer-Verlag. doi: 10.1007/s001650200003
Shield, J., Hayes, I. J. and Carrington, D. A. (2001). Using theory interpretation to mechanise the reals in a theorem prover. CATS2001, Gold Coast, 29 January-1 February, 2001. Oxford: Elsevier.
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
Shield, Jamie, Hayes, Ian and Carrington, David (2001). Using theory interpretation to mechanise the reals in a theorem prover. Computing: The Australasian Theory Symposium (CATS 2001), , , January 29, 2001-January 30, 2001. Elsevier. doi: 10.1016/S1571-0661(04)80890-9
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
Hemer, David, Hayes, Ian and Strooper, Paul (2001). Refinement calculus for logic programming in Isabelle/HOL. Springer Verlag.
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
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
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
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
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
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
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.
Colvin, R., Hayes, I. J. and Strooper, P. (1998). Data refining logic programs. International Refinement Workshop and Formal Methods Pacific '98, Canberra, Australia, 29 September - 2 October, 1998. New York: Springer -Verlag.
Fidge, C. J., Hayes, I. J., Martin, A. P. and Wabenhorst, A. K. (1998). A set-theoretic model for real-time specification and reasoning. 4th International Conference on Mathematics of Program Construction, MPC 1998, Marstrand, June 15- 17 1998. Germany: Springer Verlag. doi: 10.1007/bfb0054291
Fidge, C. J., Hayes, I. J. and Mahony, B. P. (1998). Defining differentiation and integration in Z. 2nd International Conference on Formal Engineering Methods, ICFEM 1998, Brisbane, QLD, December 9, 1998-December 11, 1998. Institute of Electrical and Electronics Engineers Inc.. doi: 10.1109/ICFEM.1998.730571
Colvin, R., Hayes, I., Nickson, R. and Strooper, P. (1997). A tool for logic program refinement (Extended abstract). Formal Methods Pacific Conference (FMP 97), Wellington New Zealand, 9-11 July 1997. Singapore: Springer-Verlag Singapore Pte..
Hayes, I. J., Nickson, R. G. and Strooper, P. A. (1996). Refining specifications to logic programs. Logic Program Synthesis and Transformation 6th International Workshop, LOPSTR'96, Stockholm, Sweden, August 28–30, 1996. Berlin / Heidelberg: Spinger. doi: 10.1007/3-540-62718-9_1
Fidge, C., Utting, M., Kearney, P. and Hayes, I. (1996). Integrating real-time scheduling theory and program refinement. 3rd International Symposium of Formal Methods Europe, FME 1996, Oxford, United Kingdom, 18-22 March 1996. Springer Verlag. doi: 10.1007/3-540-60973-3_95
Hayes, Ian and Utting, Mark (1996). Coercing real-time refinement: a transmitter. BCS-FACS Northern Formal Methods Workshop, Ilkley, United Kingdom, 23-24 September 1996. BCS Learning & Development. doi: 10.14236/ewic/fa1996.9
Bakker Paul, Carrington David, Goodchild Andrew, Hayes Ian, Purchase Helen and Strooper Paul (1995). Communicating technologist: an educational challenge. Proceedings of the 1995 25th Annual Conference on Frontiers in Education. Part 1 (of 2), Atlanta, GA, USA, November 1, 1995-November 4, 1995. doi: 10.1109/fie.1995.483173
Bancroft, Peter and Hayes, Ian (1995). A formal semantics for a language with type extension. 9th International Conference of Z Users Meeting, ZUM 1995, Limerick Ireland, 7- 9 September 1995. Germany: Springer Verlag.
Hayes, I., Araki, K., Duke, D. and Veraart, V. (1995). Are formal methods relevant?. Institute of Electrical and Electronics Engineers Inc.. doi: 10.1109/APSEC.1995.497003
Carrington, David, Duke, David, Hayes, Ian and Welsh, Jim (1993). Deriving modular designs from formal specifications. 1st ACM SIGSOFT Symposium on Foundations of Software Engineering, SIGSOFT 1993, Los Angeles, CA, 8 - 10 December 1993. New York, NY United States: Association for Computing Machinery. doi: 10.1145/256428.167066
Hayes, Ian and Wildman, Luke (1993). Towards Libraries for Z. Z User Workshop, London 1992, London, United Kingdom, 14–15 December 1992. London: Springer London. doi: 10.1007/978-1-4471-3556-2_3
Mahony, Brendan and Hayes, Ian (1991). A Case Study in Timed Refinement: A Central Heater. 4th Refinement Workshop, Cambridge, United Kingdom, 9–11 January 1991. London: Springer London. doi: 10.1007/978-1-4471-3756-6_8
Hayes, Ian (1991). Interpretations of Z Schema Operators. Z User Workshop, Oxford 1990 , Oxford United Kingdom, 17–18 December 1990. London: Springer London. doi: 10.1007/978-1-4471-3540-1_2
Hayes, Ian (1990). A Generalisation of Bags in Z. Z User Workshop , Oxford, , 15 December 1989. London: Springer London. doi: 10.1007/978-1-4471-3877-8_7
Hayes I.J. (1986). Using mathematics to specify software. First Australian Software Engineering Conference. Software Engineering: Path to Computer Systems Reliability, Canberra, Aust, *. Inst of Engineers.
Data Collection
Dongol, Brijesh M.S., Hayes, Ian J. and Robinson, Peter J. (2013). Prolog. The University of Queensand. (Dataset) doi: 10.14264/uql.2014.173
Department Technical Reports
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.
Colvin, Robert and Hayes, Ian J. (2010). A semantics for behavior trees. Systems and Software Engineering Technical Reports, SSE-2010-03. School of Information Technol and Elec Engineering, University of Queensland.
Colvin, Robert and Hayes, Ian J. (2010). Structural operational semantics through context-dependent behaviour. Systems and Software Engineering Technical Reports, SSE-2010-02. School of Information Technology and Electrical Engineering, The University of Queensland.
Dongol, Brijesh, Hayes, Ian J. and Robinson, Peter J. (2009). Reasoning about real-time teleo-reactive programs. Technical Report SSE-2010-01. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
Brijesh Dongol and Ian J. Hayes (2007). Trace Semantics for the Owicki-Gries Theory Integrated with the Progress Logic from UNITY. SSE Technical Reports, Technical Report SSE-2007-02. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
Hayes, Ian J. and Meinicke, Larissa (2006). Reasoning Algebraically about Probabilistic Loops. Technical Report SSE-2006-02. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
Meinicke, Larissa and Hayes, Ian J. (2006). Algebraic Reasoning for Probabilistic Action Systems and While-Loops. Technical Report SSE-2006-05. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
Cook, Phil, Welsh, Jim and Hayes, Ian J. (2005). Incremental Semantic Evaluation for Interactive Systems: Inertia, Pre-emption, and Relations. Technical Report SSE-2005-01. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
Cook, Phil, Welsh, Jim and Hayes, Ian J. (2005). Building a Flexible Incremental Compiler Back-End. Technical Report SSE-2005-02. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
Lermer, Karl, Fidge, Colin and Hayes, Ian (2002). Linear Approximation of Execution Time Constraints. Technical Report 02-31. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Peuker, Sibylle and Hayes, Ian (2002). Timing Analysis of Concurrent Real-Time Programs With Deadlines. Technical Report 02-37. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Cook, Phil, Welsh, Jim and Hayes, Ian J. (2002). Incremental Context-Sensitive Evaluation in Context. Technical Report 02-11. Software Verification Research Centre, The University of Queensland.
Lermer, Karl, Fidge, Colin and Hayes, Ian (2002). Formal Semantics for Program Paths. Technical Report 02-05. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Lermer, Karl, Fidge, Colin and Hayes, Ian (2002). A Theory for Execution Time Derivation in Real-time Programs. Technical Report 02-13. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Colvin, Robert, Hemer, David, Hayes, Ian and Strooper, Paul (2001). Translating Refined Logic Programs to Mercury. Technical Report no. 01-32. Software Verification Research Centre, School of Information Technology, The University Of Queensland.
Hemer, D. G., Colvin, R., Hayes, I. J. and Strooper, P. A. (2001). Don't care non-determinism in logic program refinement. SRV Techical Report No. 01-27. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Hayes, Ian, Nickson, Ray, Strooper, Paul and Colvin, Robert (2000). A Declarative Semantics for Logic Program Refinement. Technical Report no. 00-30. Software Verification Research Centre, School of Information Technology, The University of Queensland.
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.
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.
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.
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.
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.
Carrington, D., Hayes, I., Nickson, R., Watson, G. N. and Welsh, J. (1996). A Tool for Developing Correct Programs by Refinement. technical Report no. 95-49. Software Verification Research Centre, School of Information Technology, The University of Queensland.
Research Reports
Hayes, I. J. (2002). Block-structured (attribute) grammars. Brisbane, Australia: The University of Queensland.
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.