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.
Journal Article: Deriving real-time action systems with multiple time bands using algebraic reasoning
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.
Conference Publication: Invariants, well-founded statements and real-time program algebra
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.
Conference Publication: Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions
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.
An extensible framework for analysis of Java language-based security conformance
(2014–2016) ARC Linkage Projects
Understanding concurrent programs using rely-guarantee thinking
(2013–2015) ARC Discovery Projects
Software Quality Improvement Through Static Analysis and Annotation
(2011–2014) ARC Linkage Projects
Transformation Rules for Probabilistic Programs: An Algebraic Approach
(2008) Doctor Philosophy
Progress-based verification and derivation of concurrent programs
(2009) Doctor Philosophy
(2009) Doctor Philosophy
Refining logic programs using types and invariants
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.
Semantic identification of dead control-flow paths
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.
Real-time specification and reasoning using maximal intervals
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.
Defining Differentiation and Integration in Z
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.
Dynamically detecting faults via integrity constraints
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.
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. In Jones, C. B., Liu, Z. and Woodcock, J. (Ed.), Formal Methods and Hybrid Real-Time Systems (pp. 364-390) Berlin, Germany: Springer-Verlag.
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. In Maurice Bruynooghe and Kunk-Kiu Lau (Ed.), Program Development in Computational Logic (pp. 66-89) Berlin: Springer Verlag.
A predicative semantics for real-time refinement
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.
Specifications are not (necessarily) executable
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.
Deriving real-time action systems with multiple time bands using algebraic reasoning
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.
Deriving real-time action systems in a sampling logic
Dongol, Brijesh and Hayes, Ian J. (2013) Deriving real-time action systems in a sampling logic. Science of Computer Programming, 78 11: 2047-2063.
Linking unifying theories of program refinement
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.
Comparing degrees of non-Determinism in expression evaluation
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.
Reasoning about goal-directed real-time teleo-reactive programs
Dongol, Brijesh, Hayes, Ian J. and Robinson, Peter J. (2013) Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects of Computing, 26 3: 563-589.
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.
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.
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.
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.
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.
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.
A theory for execution-time derivation in real-time programs
Lermer, K., Fidge, C. J. and Hayes, I. J. (2005) A theory for execution-time derivation in real-time programs. Theoretical Computer Science, 346 1: 3-27.
Linear approximation of execution-time constraints
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.
A refinement calculus for logic programs
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.
An introduction to real-time Object-Z
Smith, G. P. and Hayes, I. J. (2002) An introduction to real-time Object-Z. Formal Aspects of computing, 13 2: 128-141.
Reasoning about real-time repetitions: terminating and nonterminating
Hayes, Ian (2002) Reasoning about real-time repetitions: terminating and nonterminating. Science of Computer Programming, 43 2-3: 161-192.
A sequential real-time refinement calculus
Hayes, I. J. and Utting, M. (2001) A sequential real-time refinement calculus. Acta Informatica, 37 6: 385-448.
Semantic characterisation of dead control-flow paths
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.
Fidge, C. J., Hayes, I. J. and Watson, G. N. (1999) The deadline command. IEE Proceedings - Software, 146 2: 104-111.
Supporting contexts in program refinement
Nickson, R and Hayes, I (1997) Supporting contexts in program refinement. Science of Computer Programming, 29 3: 279-302.
Invariants, well-founded statements and real-time program algebra
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.
Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions
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.
Path-sensitive data flow analysis simplified
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.
Visuocode: A software development environment that supports spatial navigation and composition
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.
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. 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.
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. 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.
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. 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.
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. 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.
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. 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.
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. In: Wolfram Kahl and Timothy G. Griffin, Proceedings: 13th International Conference, RAMiCS 2012. 13th International Conference, RAMiCS 2012, Cambridge, United Kingdom, (50-65). 17 - 20 September 2012.
Approximating idealised real-time specifications using time bands
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.
Compositional action system derivation using enforced properties
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.
Integrating requirements: The behavior tree philosophy
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.
Invariants and well-foundedness in program algebra
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.
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. 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.
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. 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.
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.
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. 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.
Probabilistic Choice in Refinement Algebra
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.
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. 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. SERENE '08: Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, Newcastle Upon Tyne, UK, (87-94). 17-19 Nov 2008.
Continuous action system refinement
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.
Reasoning algebraically about probabilistic loops
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.
Termination of real-time programs: Definitely, definitely not, or maybe
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.
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. 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.
Towards platform-independent real-time systems
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.
Determining the specification of a control system from that of its environment
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.
Formal Semantics for Program Paths
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.
Programs as paths: An approach to timing constraint analysis
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.
Reasoning about deadlines in concurrent real-time programs
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.
Refinement of higher-order logic programs
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.
Don't care non-determinism in logic program refinement
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.
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.
Refining object-orientated invariants and dynamic constraints
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.
The real-time refinement calculus: A foundation for machine-independent real-time programming
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.
Towards a refinement calculus for concurrent real-time programs
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.
Translating refined logic programs to Mercury
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.
A technique for modular logic program refinement
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.
Using theory interpretation to mechanise the reals in a theorem prover
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.
Real-time program refinement using auxiliary variables
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.
Reasoning about non-terminating loops using deadline commands
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.
Reasoning about real-time programs using idle-invariant assertions
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.
Refining logic programs using types
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.
Structuring real-time Object-Z specifications
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.
Structuring real-time Object-Z specifications
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.
Real-time specification and reasoning using maximal intervals
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.
A tool for logic program refinement (Extended abstract)
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.
Refining specifications to logic programs
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.
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.
Dongol, Brijesh M.S., Hayes, Ian J. and Robinson, Peter J (2013): Prolog. The University of Queensand. Dataset.
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.
Block-structured (attribute) grammars
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
An extensible framework for analysis of Java language-based security conformance
(2014–2016) ARC Linkage Projects
Understanding concurrent programs using rely-guarantee thinking
(2013–2015) ARC Discovery Projects
Software Quality Improvement Through Static Analysis and Annotation
(2011–2014) ARC Linkage Projects
(2009–2012) Griffith University
Combining Time Bands and Teleo-Reactive Programs for Advanced Dependable Real-Time Systems
(2008–2011) ARC Discovery Projects
Analysing and Generating Fault-Tolerant Real-Time Systems
(2004–2007) ARC Discovery Projects
ARC Centre for Complex Systems
(2002–2008) ARC Centres of Excellence
Building dependability into complex, computer-based systems
(2002–2003) ARC Discovery Projects
Derivation and timing analysis of concurrent real-time software
(2001–2003) ARC Discovery Projects
(2001–2002) UQ External Support Enabling Grant
Effective Real-Time Program Analysis
(1998–2001) ARC Australian Research Council (Large grants)
Refinement Calculus for Logic Programming
(1998–2001) ARC Australian Research Council (Large grants)
A unified formalism for concurrent real time software development
(1997–2000) ARC Australian Research Council (Large grants)
Refinement Calculus for Logic Programming
(1996–1997) UQ External Support Enabling Grant
Timing path analysis of high-level real-time programs
(1996–1997) ARC Australian Research Council (Small grants)
Adding flexible modularisation to the refinement calculus
(1995–1996) UQ External Support Enabling Grant
Refinement calculus for logic programming
(1995–1996) ARC Australian Research Council (Small grants)
Specification and refinement of real time control systems
(1994–1995) UQ External Support Enabling Grant
Software development visualisation
Doctor Philosophy — Principal Advisor
Other advisors:
Inference and analysis of rely-guarantee specifications for reasoning about the correctness of concurrent software systems
Doctor Philosophy — Principal Advisor
Other advisors:
Controlling the Generation of Multiple Counterexamples in LTL Model Checking
Doctor Philosophy — Principal Advisor
Other advisors:
Transformation Rules for Probabilistic Programs: An Algebraic Approach
(2008) Doctor Philosophy — Principal Advisor
Progress-based verification and derivation of concurrent programs
(2009) Doctor Philosophy — Principal Advisor
(2009) Doctor Philosophy — Principal Advisor
FORMAL PROPERTY PRESERVATION AND TRANSFORMATION IN SOFTWARE EVOLUTION
(2012) Master Philosophy — Associate Advisor
Other advisors:
INCREMENTAL COMPILATION IN LANGUAGE-BASED ENVIRONMENTS
(2006) Doctor Philosophy — Principal Advisor
Towards an object-oriented refinement calculus
(2004) Doctor Philosophy — Associate Advisor
DATA REFINEMENT AND DATA TYPES IN THE REFINEMENT CALCULUS FOR LOGIC PROGRAMS
(2002) Doctor Philosophy — Associate Advisor
Other advisors: