Professor Ian Hayes

Chair in CS&EE

School of Information Technology and Electrical Engineering
Faculty of Engineering, Architecture and Information Technology
ian.hayes@uq.edu.au
+61 7 336 52386

Overview

Software Engineering. Ian's research interests are in formal methods for software development, particularly for concurrent and real-time systems.

He is currently the head of the Systems and Software Engineering Research Group.

Qualifications

  • Bach of Science (Computer Science) Hons, University of New South Wales
  • Doctor of Philosophy (Computer Science), University of New South Wales

Publications

View all Publications

Publications

Book

  • 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.

Book Chapter

  • Hayes, Ian J. (2009). Dynamically detecting faults via integrity constraints. In Michael Butler, Cliff Jones, Alexander Romanovsky and Elena Troubitsyna (Ed.), Methods, Models, and Tools for Fault Tolerance (pp. 85-103) 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. In Jones, C. B., Liu, Z. and Woodcock, J. (Ed.), Formal Methods and Hybrid Real-Time Systems (pp. 364-390) Berlin, Germany: Springer-Verlag.

  • Colvin, Robert, Groves, Lindsay, Hayes, Ian J., Hemer, David, Nickson, Ray and Strooper, Paul (2004). Developing logic programs from specifications using stepwise refinement. In Maurice Bruynooghe and Kunk-Kiu Lau (Ed.), Program Development in Computational Logic (pp. 66-89) Berlin: Springer Verlag.

  • Hayes, I. J. (2003). A predicative semantics for real-time refinement. In A. McIver and C. Morgan (Ed.), Programming Methodology 1 ed. (pp. 109-133) New York: Springer Verlag.

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

Journal Article

Conference Publication

  • Hayes, Ian J. and Meinicke, Larissa (2014). Invariants, well-founded statements and real-time program algebra. In: Cliff Jones, Pekka Pihlajasaari and Jun Sun, FM 2014: Formal Methods - 19th International Symposium, Proceedings. 19th International Symposium on Formal Methods, FM 2014, Singapore, (318-334). 12 - 16 May 2014. doi:10.1007/978-3-319-06410-9_23

  • Hayes I.J. (2014). Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions. In: Formal Techniques for Safety-Critical Systems - 2nd International Workshop, FTSCS 2013, Revised Selected Papers. 2nd International Workshop of Formal Techniques for Safety-Critical Systems, FTSCS 2013, Queenstown, (1-2). October 29, 2013-October 30, 2013. doi:10.1007/978-3-319-05416-2_1

  • Winter, Kirsten, Zhang, Chenyi, Hayes, Ian J., Keynes, Nathan, Cifuentes, Cristina and Li, Lisa (2013). Path-sensitive data flow analysis simplified. In: Lindsay Groves and Jing Sun, Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, Proceedings. 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, (415-430). 29 October - 1 November 2013. doi:10.1007/978-3-642-41202-8_27

  • Bradley, Daniel R. and Hayes, Ian J. (2013). Visuocode: A software development environment that supports spatial navigation and composition. In: Alexandru Telea, Andreas Kerren and Andrian Marcus, 2013 First IEEE Working Conference on Software Visualization (VISSOFT) : proceedings of VISSOFT 2013. 1st IEEE Working Conference on Software Visualization, VISSOFT 2013, Eindhoven, The Netherlands, (). 27 - 28 September 2013. doi:10.1109/VISSOFT.2013.6650533

  • Dongol, Brijesh and Hayes, Ian J. (2012). Deriving real-time action systems controllers from multiscale system specifications. In: Jeremy Gibbons and Pablo Nogueira, Proceedings: Mathematics of Program Construction 11th International Conference, MPC 2012. Mathematics of Program Construction 11th International Conference, MPC 2012, Madrid, Spain, (102-131). 25 - 27 June 2012.

  • Dongol, Brijesh, Derrick, John and Hayes, Ian J. (2012). Fractional permissions and non-deterministic evaluators in interval temporal logic. In: Gerald Luettgen and Stephan Merz, Automated Verification of Critical Systems 2012. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012), Bamberg, Germany, (1-15). 18–20 September 2012.

  • Hayes, Ian J. and Colvin, Robert J. (2012). Integrated operational semantics: small-step, big-step and multi-step. In: John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves and Elvinia Riccobene, Abstract State Machines, Alloy, B, VDM, and Z: Third International Conference, ABZ 2012, Proceedings. 3rd International Conference on Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012), Pisa, Italy, (21-35). 18-21 June 2012.

  • Escott, Eban, Strooper, Paul, King, Paul and Hayes, Ian J. (2012). Model-driven web form validation with UML and OCL. In: Andreas Harth and Nora Koch, Current trends in web engineering: workshops, doctoral symposium, and tutorials, held at ICWE 2011, revised selected papers. 11th International Conference on Web Engineering (ICWE 2011), Paphos, Cyprus, (223-235). 20-21 June 2011.

  • Dongol, Brijesh and Hayes, Ian J. (2012). Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In: John Derrick, Stefania Gnesi, Diego Latella and Helen Treharne, Integrated Formal Methods: 9th International Conference, IFM 2012, proceedings. 9th International Conference on Integrated Formal Methods (IFM 2012), Pisa, Italy, (39-53). 18-21 June 2012.

  • Dongol, Brijesh, Hayes, Ian J., Meinicke, Larissa and Solin, Kim (2012). Towards an algebra for real-time programs. In: Wolfram Kahl and Timothy G. Griffin, Proceedings: 13th International Conference, RAMiCS 2012. 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012), Cambridge, United Kingdom, (50-65). 17 - 20 September 2012. doi:10.1007/978-3-642-33314-9_4

  • Dongol, Brijesh and Hayes, Ian J. (2011). Approximating idealised real-time specifications using time bands. In: Alexander Romanovsky, Cliff Jones, Jens Bendisposto and Michael Leuschel, Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011). 11th International Workshop on Automated Verification of Critical Systems, Newcastle upon Tyne, United Kingdom, (1-16). 12-14 September 2011.

  • Dongol, Brijesh and Hayes, Ian J. (2010). Compositional action system derivation using enforced properties. In: Claude Bolduc, Jules Desharnais and Béchir Ktari, Lecture Notes in Computer Science. Mathematics of Program Construction: 10th International Conference, MPC 2010. Mathematics of Program Construction [MPC], Quebec City, Quebec, Canada, (119-139). 21-23 June, 2010. doi:10.1007/978-3-642-13321-3_9

  • Winter, Kirsten, Hayes, Ian J. and Colvin, Robert (2010). Integrating requirements: The behavior tree philosophy. In: Proceedings of International Conference on Software Engineering and Formal Methods (SEFM 2010). Software Engineering and Formal Methods (SEFM 2010), Pisa, Italy, (41-50). 13-18 September 2010. doi:10.1109/SEFM.2010.13

  • Hayes, Ian J. (2010). Invariants and well-foundedness in program algebra. In: Ana Cavalcanti, David Deharbe, Marie-Claude Gaudel and Jim Woodcock, Theoretical Aspects of Computing – ICTAC 2010: 7th International Colloquium proceedings. 7th International Colloquium on Theoretical Aspects of Computing (ICTAC 2010), Natal, Rio Grande do Norte, Brazil, (1-14). 1-3 September 2010. doi:10.1007/978-3-642-14808-8_1

  • Dunne, Steve E., Hayes, Ian J. and Galloway, Andy J. (2010). Reasoning about loops in total and general correctness. In: Andrew Butterfield, UTP 2008: Revised Selected Papers. Unifying Theories of Programming: Second International Symposium, UTP 2008, Dublin, Ireland, (62-81). 8-10 September, 2008. 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. In: Claude Bolduc, Jules Desharnais and Béchir Ktari, Lecture Notes in Computer Science. Mathematics of Program Construction: 10th International Conference, MPC 2010. Mathematics of Program Construction [MPC], Québec City, Québec, Canada, (178-194). 21-23 June, 2010. doi:10.1007/978-3-642-13321-3

  • Colvin, Robert and Hayes, Ian J. (2009). CSP with hierarchical state. In: Lecture NOtes in Computer Science: Integrated Formal Methods. 7th International Conference on Integrated Formal Methods: IFM 2009, Dusseldorf, Germany, (118-135). 16-19 February 2009. doi:10.1007/978-3-642-00255-7_9

  • Dongol, Brijesh and Hayes, Ian J. (2009). Enforcing safety and progress properties: An approach to concurrent program derivation. In: Colin Fidge, Proceedings: Australian Software Engineering Conference, 2009. ASWEC '09. Australian Software Engineering Conference [ASWEC], Gold Coast , Australia, (3-12). 14-17 April 2009. doi:10.1109/ASWEC.2009.12

  • Meinicke, L. and Hayes, I. J. (2008). Probabilistic Choice in Refinement Algebra. In: P. Audebaud and C. Paulin-Mohring, Lecture Notes in Computer ScienceProceedings of the 9th international conference on Mathematics of Program Construction. 9th International Conference on Mathematics of Program Construction [MPC], Marseille, France, (243-267). 15-18 July 2008. doi:10.1007/978-3-540-70594-9_14

  • Hayes, I.J. (2008). Towards reasoning about teleo-reactive programs for robust real-time systems. In: Guelfi, N., Muccini, H., Pelliccione, P. and Romanovsky, A., Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems. 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems (SERENE '08), Newcastle Upon Tyne, UK, (87-94). 17-19 Nov 2008. doi:10.1145/1479772.1479789

  • Meinicke, L. A. and Hayes, I. J. (2006). Continuous action system refinement. In: Tarmo Uustalu, Mathematics of Program Construction. 8th International Conference on Mathematics of Program Construction (MPC 2006), Kuressaare, Estonia, (316-337). 3-5 July 2006.

  • Meinicke, Larissa and Hayes, Ian J. (2006). Reasoning algebraically about probabilistic loops. In: Z. Liu and J. He, 8th International Conference on Formal Engineering Methods, Macua, PR China, (380-399). 1-3 November, 2006. doi:10.1007/11901433

  • Hayes, I. J. (2006). Termination of real-time programs: Definitely, definitely not, or maybe. In: S. Dunne and B. Stoddart, Unifying Theories of Programming. First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, (141-154). 5 - 7 February, 2006. doi:10.1007/11768173_9

  • Glynn, Erica, Hayes, Ian and Macdonald, Anthony (2005). Integration of generic program analysis tools into a software development environment. In: V. Estivill-Castro, ACSC '05 Proceedings of the Twenty-eighth Austalasian Conference on Computer Science. Twenty-Eighth Australasian Conference Computer Science, Newcastle, NSW, (249-257). 31 Jan - 3 Feb 2005.

  • Hayes, I. J. (2004). Towards platform-independent real-time systems. In: P. Strooper, Proceedings: 2004 Australian Software Engineering Conference (ASWEC 2004). The 2004 Australian Software Engineering Conference (ASWEC 2004), Melbourne, Australia, (192-200). 13-16 April 2004. doi:10.1109/ASWEC.2004.1290472

  • Hayes, I. J., Jackson, M. A. and Jones, C. B. (2003). Determining the specification of a control system from that of its environment. In: K. Araki, S. Gnesi and D. Mandrioli, Lecture Notes in Computer Science. FME 2003: Formal Methods. International Symposium of Formal Methods Europe, Pisa, Italy, (154-169). 8-14 September 2003. doi:10.1007/b13229

  • Lermer, Karl, Fidge, Colin and Hayes, Ian J. (2003). Formal Semantics for Program Paths. In: James Hartland, Electronic Notes in Theoretical Computer Science. CATS'03, Computing: the Australasian Theory Symposium. Computing: The Australasian Theory Symposium [CATS], Adelaide, (58-81). 4-7 February 2003. doi:10.1016/S1571-0661(04)81006-5

  • Hayes, I. J. (2003). Programs as paths: An approach to timing constraint analysis. In: J. Dong and J. Woodcock, Proceedings of the Fifth International Conference on Formal Engineering Methods. The Fifth International Conference on Formal Engineering Methods, Singapore, (1-15). 5-7 November, 2003. doi:10.1007/b94115

  • Peuker, S. and Hayes, I. J. (2003). Reasoning about deadlines in concurrent real-time programs. In: M. Charpentier and B. Sanders, Proceedings of the International Parallel and Distributed Processing Symposium 2003. International Parallel and Distributed Processing Symposium 2003, Nice, France, (1-8). 22-26 April 2003.

  • Colvin, Robert, Hayes, Ian J., Hemer, David G. and Strooper, Paul A. (2003). Refinement of higher-order logic programs. In: M. Leuschel, Lecture Notes in Computer Science. Logic Based Program Synthesis and Transformation. Proceedings of the Twelfth International Workshop. The Twelfth International Symposium on Logic-based Program Synthesis and Transformation, Madrid, Spain, (126-143). 17-20 September 2002. doi:10.1007/3-540-45013-0_11

  • Hemer, David, Colvin, Robert, Hayes, Ian and Strooper, Paul (2002). Don't care non-determinism in logic program refinement. In: James Harland, Electronic Notes in Theoretical Computer Science: Proceedings of the Australasian Theory Symposium. CATS'02, Computing: the Australasian Theory Symposium, Amsterdam, Denmark, (101-121). 28 January - 1 February 2002. doi:10.1016/S1571-0661(04)00308-1

  • Hayes, I. J. (2002). Reasoning about timeouts. In: E. Boiten and B. Moller, Mathematics of Program Construction. Sixth International Conference, MPC 2002, Dagstuhl, Germany, (21-40). 8-10 July, 2002. doi:10.1007/3-540-45442-X_7

  • Shield, J. and Hayes, I. J. (2002). Refining object-orientated invariants and dynamic constraints. In: P. Strooper and P. Muenchaisri, Asia-Pacific Software Engineering Conference. Ninth Asia-Pacific Software Engineering Conference, The Gold Coast, (52-61). 4-6 December, 2002.

  • Hayes, I. J. (2002). The real-time refinement calculus: A foundation for machine-independent real-time programming. In: J. Esparza and C. Lakos, Application and Theory of Petri Nets 2002. Application and Theory of Petri Nets 2002, 23rd International Conference ICATPN, Adelaide, Australia, (44-58). 24-30 June, 2002.

  • Peuker, S. and Hayes, I. J. (2002). Towards a refinement calculus for concurrent real-time programs. In: C. George and H. Miao, 4th International Conference on Formal Engineering Methods, ICFEM 2002. ICFEM 2002, Shanghai, China, (335-347). 21-25th October, 2002.

  • Colvin, R., Hayes, I. J., Hemer, D. G. and Strooper, P. A. (2002). Translating refined logic programs to Mercury. In: M. Oudshoorn, Proceedings of the Twenty-Fifth Australasian Computer Science Conference - Computer Science 2002. ACSC 2002, Melbourne, Australia, (33-40). 28 January - 1 February, 2002.

  • Colvin, Robert, Hayes, Ian and Strooper, Paul (2001). A technique for modular logic program refinement. In: K. Lau, Lecture Notes in Computer Science: Proceedings of the Tenth International Workshop on Logic Based Program Synthesis and Transformation. Tenth International Workshop on Logic-Based Program Synthesis and Transformation, London, England, (38-56). 24-28 July, 2001. doi:10.1007/3-540-45142-0_3

  • Shield, J., Hayes, I. J. and Carrington, D. A. (2001). Using theory interpretation to mechanise the reals in a theorem prover. In: C.J Fidge, Proceedings of Computing: The Australian Theory Symposium (CATS2001). CATS2001, Gold Coast, (266-281). 29 January-1 February, 2001.

  • Hayes, I. J. (2000). Real-time program refinement using auxiliary variables. In: M. Joseph, Proceedings 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: FTRTFT 2000. Formal Techniques in Real-Time and Fault-Tolerant Systems, 6th International Symposium, Pune, India, (170-184). 20-22 September 2000.

  • Hayes, I. J. (2000). Reasoning about non-terminating loops using deadline commands. In: R. Backhouse and J. N. Oliveira, Lecture notes in computer science: 5th International Conference on Mathematics of Program Construction: MPC 2000. MPC 2000, Ponte de Lima, Portugal, (60-79). 3-5 July 2000. doi:10.1007/10722010_5

  • Hayes, I. J. (2000). Reasoning about real-time programs using idle-invariant assertions. In: Proceedings of IEEE: 7th Asia-Pacific Software Engineering Conference (APSEC 2000). APSEC 2000, Singapore, (16-23). 5-8 December 2000. doi:10.1109/APSEC.2000.896678

  • Colvin, Robert, Hayes, Ian J. and Strooper, Paul A. (2000). Refining logic programs using types. In: Jenny Edwards, Proceedings 23rd Australasian Computer Science Conference: ACSC 2000. ACSC 2000, Canberra, ACT, Australia, (43-50). 31 January - 3 February, 2000. doi:10.1109/ACSC.2000.824379

  • Smith, G. P. and Hayes, I. J. (2000). Structuring real-time Object-Z specifications. In: W. Grieskamp, T. Santen and B. Stoddart, Lecture notes in computer science: Integrated Formal Methods. Integrated Formal Methods: Second International Conference, IFM 2000, Schloss Dagstuhl, Germany, (97-115). 1-3 November, 2000.

  • Smith, G and Hayes, I (2000). Structuring real-time Object-Z specifications. In: Lecture Notes in Computer Science 1945. Integrated Formal Methods: Second International Conference, IFM 2000,, Dagstuhl Castle, Germany, (97-115). November 2000.

  • Fidge, C. J., Hayes, I. J., Mahony, B. and Wabenhorst, A. K. (1999). Real-time specification and reasoning using maximal intervals. In: W. C. H. Cheng and A. S. M. Sajeev, 6th Australasian Conference on Parallel and Real-Time Systems. PART '99, Melbourne, Australia, (344-354). 29 Nov - 1 Dec 1999.

  • Smith, G. P. and Hayes, I. J. (1999). Towards real-time Object-Z. In: K. Araki, A. Galloway and K. Taguchi, Proceedings of the 1st International Conference on Integrated Formal Methods. Integrated Formal Methods IFM'99, York, UK, (49-65). 28-29 June, 1999.

  • Colvin, R., Hayes, I. J. and Strooper, P. (1998). Data refining logic programs. In: Jim Grundy, Martin Schwenke and Trevor Vickers, Proceedings of IRW/FMP. International Refinement Workshop and Formal Methods Pacific '98, Canberra, Australia, (100-116). 29 September - 2 October, 1998.

  • Colvin, R., Hayes, I., Nickson, R. and Strooper, P. (1997). A tool for logic program refinement (Extended abstract). In: Formal Methods Pacific Conference 1997. Formal Methods Pacific Conference (FMP 97), Wellington New Zealand, (289-290). 9-11 July 1997.

  • Hayes, I. J., Nickson, R. G. and Strooper, P. A. (1996). Refining specifications to logic programs. In: Lecture Notes in Computer Science: Logic Program Synthesis and Transformation. Logic Program Synthesis and Transformation 6th International Workshop, LOPSTR'96, Stockholm, Sweden, (1-19). August 28–30, 1996. doi:10.1007/3-540-62718-9_1

Edited Outputs

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

Other Outputs

  • Dongol, Brijesh M.S., Hayes, Ian J. and Robinson, Peter J. (2013): Prolog. The University of Queensand. Dataset. doi:10.14264/uql.2014.173. doi:doi:10.14264/uql.2014.173

  • 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.

  • Hayes, I. J. (2002) Block-structured (attribute) grammars Brisbane, Australia: The University of Queensland

  • Hayes, Ian J. and Utting, Mark (1998) Deadlines are termination St Lucia, QLD, Australia: Software Verification Research Centre, School of Information Technology, The University of Queensland

Grants (Administered at UQ)

PhD and MPhil Supervision

Current Supervision

  • Doctor Philosophy — Principal Advisor

  • Doctor Philosophy — Principal Advisor

    Other advisors:

  • Doctor Philosophy — Principal Advisor

    Other advisors:

Completed Supervision