| 2023 | CPP | Verifying Term Graph Optimizations using Isabelle/HOL. | Brae J. Webb, Ian J. Hayes, Mark Utting |
| 2023 | ICFEM | Trace Models of Concurrent Valuation Algebras. | Nasos Evangelou-Oost, Larissa Meinicke, Callum Bannister, Ian J. Hayes |
| 2023 | ICFEM | Verifying Compiler Optimisations - (Invited Paper). | Ian J. Hayes, Mark Utting, Brae J. Webb |
| 2021 | ATVA | A Formal Semantics of the GraalVM Intermediate Representation. | Brae J. Webb, Mark Utting, Ian J. Hayes |
| 2019 | MPC | Cylindric Kleene Lattices for Program Construction. | Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth |
| 2018 | FM | Encoding Fairness in a Synchronous Concurrent Program Algebra. | Ian J. Hayes, Larissa A. Meinicke |
| 2018 | ICFEM | Engineering a Theory of Concurrent Programming. | Ian J. Hayes |
| 2018 | ICFEM | Type Capabilities for Object-Oriented Programming Languages. | Xi Wu, Yi Lu, Patrick A. Meiring, Ian J. Hayes, Larissa A. Meinicke |
| 2017 | APLAS | Capabilities for Java: Secure Access to Resources. | Ian J. Hayes, Xi Wu, Larissa A. Meinicke |
| 2016 | FM | An Algebra of Synchronous Atomic Steps. | Ian J. Hayes, Robert J. Colvin, Larissa A. Meinicke, Kirsten Winter, Andrius Velykis |
| 2014 | FM | Invariants, Well-Founded Statements and Real-Time Program Algebra. | Ian J. Hayes, Larissa Meinicke |
| 2013 | ICFEM | Path-Sensitive Data Flow Analysis Simplified. | Kirsten Winter, Chenyi Zhang, Ian J. Hayes, Nathan Keynes, Cristina Cifuentes, Lian Li |
| 2013 | VISSOFT | Visuocode: A software development environment that supports spatial navigation and composition. | Daniel R. Bradley, Ian J. Hayes |
| 2012 | IFM | Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. | Brijesh Dongol, Ian J. Hayes |
| 2012 | MPC | Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. | Brijesh Dongol, Ian J. Hayes |
| 2011 | ICWE | Model-Driven Web Form Validation with UML and OCL. | Eban Escott, Paul A. Strooper, Paul King, Ian J. Hayes |
| 2010 | ICTAC | Invariants and Well-Foundedness in Program Algebra. | Ian J. Hayes |
| 2010 | MPC | Compositional Action System Derivation Using Enforced Properties. | Brijesh Dongol, Ian J. Hayes |
| 2010 | MPC | Unifying Theories of Programming That Distinguish Nontermination and Abort. | Ian J. Hayes, Steve Dunne, Larissa Meinicke |
| 2010 | SEFM | Integrating Requirements: The Behavior Tree Philosophy. | Kirsten Winter, Ian J. Hayes, Robert Colvin |
| 2009 | IFM | CSP with Hierarchical State. | Robert Colvin, Ian J. Hayes |
| 2008 | MPC | Probabilistic Choice in Refinement Algebra. | Larissa Meinicke, Ian J. Hayes |
| 2006 | ICFEM | Reasoning Algebraically About Probabilistic Loops. | Larissa Meinicke, Ian J. Hayes |
| 2006 | MPC | Continuous Action System Refinement. | Larissa Meinicke, Ian J. Hayes |
| 2003 | FM | Determining the Specification of a Control System from That of Its Environment. | Ian J. Hayes, Michael A. Jackson, Cliff B. Jones |
| 2003 | ICFEM | Programs as Paths: An Approach to Timing Constraint Analysis. | Ian J. Hayes |
| 2002 | APSEC | Refining Object-Oriented Invariants and Dynamic Constraints. | Jamie Shield, Ian J. Hayes |
| 2002 | ICFEM | Towards a Refinement Calculus for Concurrent Real-Time Programs. | Sibylle Peuker, Ian J. Hayes |
| 2002 | LOPSTR | Refinement of Higher-Order Logic Programs. | Robert Colvin, Ian J. Hayes, David Hemer, Paul A. Strooper |
| 2002 | MPC | Reasoning about Timeouts. | Ian J. Hayes |
| 2000 | APSEC | Reasoning about real-time programs using idle-invariant assertions. | Ian J. Hayes |
| 2000 | IFM | Structuring Real-Time Object-Z Specifications. | Graeme Smith, Ian J. Hayes |
| 2000 | LOPSTR | Modular Logic Program Refinement. | Robert Colvin, Ian J. Hayes, Paul A. Strooper |
| 2000 | LOPSTR | A Technique for Modular Logic Program Refinement. | Robert Colvin, Ian J. Hayes, Paul A. Strooper |
| 2000 | MPC | Reasoning about Non-terminating Loops Using Deadline Commands. | Ian J. Hayes |
| 1999 | IFM | Towards Real-Time Object-Z. | Graeme Smith, Ian J. Hayes |
| 1998 | ICFEM | Defining Differentiation and Integration in Z. | Colin J. Fidge, Ian J. Hayes, Brendan P. Mahony |
| 1998 | MPC | A Set-Theoretic Model for Real-Time Specification and Reasoning. | Colin J. Fidge, Ian J. Hayes, Andrew P. Martin, Axel Wabenhorst |
| 1996 | FM | Integrating Real-Time Scheduling Theory and Program Refinement. | Colin J. Fidge, Mark Utting, Peter Kearney, Ian J. Hayes |
| 1996 | LOPSTR | Refining Specifications to Logic Programs. | Ian J. Hayes, R. G. Nickson, Paul A. Strooper |
| 1995 | APSEC | Are Formal Methods Relevant? | Ian J. Hayes, Keijiro Araki, David J. Duke, Val E. Veraart |