Some remarks on "Ambiguous Machine Architecture". - Ian J. Hayes (SIGARCH Comput. Archit. News, 1978)

Applying Formal Specification to Software Development in Industry. - Ian J. Hayes (IEEE Trans. Software Eng., 1985)

Specification Directed Module Testing. - Ian J. Hayes (IEEE Trans. Software Eng., 1986)

Laws of Programming. - C. A. R. Hoare; Ian J. Hayes; Jifeng He 001; Carroll Morgan; A. W. Roscoe 001; Jeff W. Sanders; Ib Holm Sørensen; J. Michael Spivey; Bernard Sufrin (Commun. ACM, 1987)

Signalling System No.7, The Network Layer. - Ian J. Hayes; M. Mowbray; Gordon A. Rose (PSTV, 1989)

A Generalisation of Bags in Z. - Ian J. Hayes (Z User Workshop, 1989)

Interpretations of Z Schema Operations. - Ian J. Hayes (Z User Workshop, 1990)

Towards Libraries for Z. - Ian J. Hayes; Luke Wildman (Z User Workshop, 1992)

Multi-Relations in Z. - Ian J. Hayes (Acta Informatica, 1992)

VDM and Z: A Comparative Case Study. - Ian J. Hayes (Formal Aspects Comput., 1992)

A Case-Study in Timed Refinement: A Mine Pump. - Brendan P. Mahony; Ian J. Hayes (IEEE Trans. Software Eng., 1992)

Deriving Modular Designs from Formal Specifications. - David A. Carrington; David J. Duke; Ian J. Hayes; Jim Welsh (SIGSOFT FSE, 1993)

Understanding the differences between VDM and Z. - Ian J. Hayes; Cliff B. Jones; John E. Nicholls (ACM SIGSOFT Softw. Eng. Notes, 1994)

Are Formal Methods Relevant? - Ian J. Hayes; Keijiro Araki; David J. Duke; Val E. Veraart (APSEC, 1995)

A Formal Semantics for a Language with Type Extension. - Peter Bancroft; Ian J. Hayes (ZUM, 1995)

Using Units of Measurement in Formal Specifications. - Ian J. Hayes; Brendan P. Mahony (Formal Aspects Comput., 1995)

Specification by Interface Separation. - Ian J. Hayes; Jeff W. Sanders (Formal Aspects Comput., 1995)

Integrating Real-Time Scheduling Theory and Program Refinement. - Colin J. Fidge; Mark Utting; Peter Kearney; Ian J. Hayes (FME, 1996)

Refining Specifications to Logic Programs. - Ian J. Hayes; R. G. Nickson; Paul A. Strooper (LOPSTR, 1996)

Supporting Module Reuse in Refinement. - Ian J. Hayes (Sci. Comput. Program., 1996)

Supporting Contexts in Program Refinement. - Ray Nickson; Ian J. Hayes (Sci. Comput. Program., 1997)

Defining Differentiation and Integration in Z. - Colin J. Fidge; Ian J. Hayes; Brendan P. Mahony (ICFEM, 1998)

A Set-Theoretic Model for Real-Time Specification and Reasoning. - Colin J. Fidge; Ian J. Hayes; Andrew P. Martin; Axel Wabenhorst (MPC, 1998)

Deadlines are termination. - Ian J. Hayes; Mark Utting (PROCOMET, 1998)

A Program Refinement Tool. - David A. Carrington; Ian J. Hayes; Ray Nickson; Geoffrey Watson; Jim Welsh (Formal Aspects Comput., 1998)

Expressive Power of Specification Languages. - Ian J. Hayes (Formal Aspects Comput., 1998)

Towards Real-Time Object-Z. - Graeme Smith 001; Ian J. Hayes (IFM, 1999)

The deadline command. - Colin J. Fidge; Ian J. Hayes; Geoffrey Watson (IEE Proc. Softw., 1999)

Refining Logic Programs Using Types. - Robert Colvin; Ian J. Hayes; Paul A. Strooper (ACSC, 2000)

Reasoning about real-time programs using idle-invariant assertions. - Ian J. Hayes (APSEC, 2000)

Real-Time Program Refinement Using Auxiliary Variables. - Ian J. Hayes (FTRTFT, 2000)

Structuring Real-Time Object-Z Specifications. - Graeme Smith 001; Ian J. Hayes (IFM, 2000)

Modular Logic Program Refinement. - Robert Colvin; Ian J. Hayes; Paul A. Strooper (LOPSTR, 2000)

A Technique for Modular Logic Program Refinement. - Robert Colvin; Ian J. Hayes; Paul A. Strooper (LOPSTR (LNCS 2042: Selected Papers), 2000)

Reasoning about Non-terminating Loops Using Deadline Commands. - Ian J. Hayes (MPC, 2000)

Refinement Calculus for Logic Programming in Isabelle/HOL. - David Hemer; Ian J. Hayes; Paul A. Strooper (TPHOLs, 2001)

A sequential real-time refinement calculus. - Ian J. Hayes; Mark Utting (Acta Informatica, 2001)

Semantic characterisation of dead control-flow paths. - Ian J. Hayes; Colin J. Fidge; Karl Lermer (IEE Proc. Softw., 2001)

Using Theory Interpretation to Mechanise the Reals in a Theorem Prover. - Jamie Shield; Ian J. Hayes; David A. Carrington (CATS, 2001)

Translating Refined Logic Programs to Mercury. - Robert Colvin; Ian J. Hayes; David Hemer; Paul A. Strooper (ACSC, 2002)

The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming. - Ian J. Hayes (ICATPN, 2002)

Refining Object-Oriented Invariants and Dynamic Constraints. - Jamie Shield; Ian J. Hayes (APSEC, 2002)

Towards a Refinement Calculus for Concurrent Real-Time Programs. - Sibylle Peuker; Ian J. Hayes (ICFEM, 2002)

Refinement of Higher-Order Logic Programs. - Robert Colvin; Ian J. Hayes; David Hemer; Paul A. Strooper (LOPSTR, 2002)

Reasoning about Timeouts. - Ian J. Hayes (MPC, 2002)

Don't Care Non-determinism in Logic Program Refinement. - David Hemer; Ian J. Hayes; Paul A. Strooper; Robert Colvin (CATS, 2002)

An Introduction to Real-Time Object-Z. - Graeme Smith 001; Ian J. Hayes (Formal Aspects Comput., 2002)

Reasoning about real-time repetitions: terminating and nonterminating. - Ian J. Hayes (Sci. Comput. Program., 2002)

A refinement calculus for logic programs. - Ian J. Hayes; Robert Colvin; David Hemer; Paul A. Strooper; Ray Nickson (Theory Pract. Log. Program., 2002)

Determining the Specification of a Control System from That of Its Environment. - Ian J. Hayes; Michael A. Jackson 001; Cliff B. Jones (FME, 2003)

Programs as Paths: An Approach to Timing Constraint Analysis. - Ian J. Hayes (ICFEM, 2003)

Reasoning about Deadlines in Concurrent Real-Time Programs. - Sibylle Peuker; Ian J. Hayes (IPDPS, 2003)

Formal Semantics for Program Paths. - Karl Lermer; Colin J. Fidge; Ian J. Hayes (CATS, 2003)

Linear Approximation of Execution-Time Constraints. - Karl Lermer; Colin J. Fidge; Ian J. Hayes (Formal Aspects Comput., 2003)

Towards Platform-Independent Real-Time Systems. - Ian J. Hayes (Australian Software Engineering Conference, 2004)

An Environment for Building a System out of its Requirements. - Cameron Smith; Kirsten Winter; Ian J. Hayes; R. Geoff Dromey; Peter A. Lindsay; David A. Carrington (ASE, 2004)

Developing Logic Programs from Specifications Using Stepwise Refinement. - Robert Colvin; Lindsay Groves; Ian J. Hayes; David Hemer; Ray Nickson; Paul A. Strooper (Program Development in Computational Logic, 2004)

Integration of generic program analysis tools into a software development environment. - Erica Glynn; Ian J. Hayes; Anthony MacDonald (ACSC, 2005)

A theory for execution-time derivation in real-time programs. - Karl Lermer; Colin J. Fidge; Ian J. Hayes (Theor. Comput. Sci., 2005)

Reasoning Algebraically About Probabilistic Loops. - Larissa Meinicke; Ian J. Hayes (ICFEM, 2006)

Continuous Action System Refinement. - Larissa Meinicke; Ian J. Hayes (MPC, 2006)

Termination of Real-Time Programs: Definitely, Definitely Not, or Maybe. - Ian J. Hayes (UTP, 2006)

Deriving Specifications for Systems That Are Connected to the Physical World. - Cliff B. Jones; Ian J. Hayes; Michael A. Jackson 001 (Formal Methods and Hybrid Real-Time Systems, 2007)

Procedures and parameters in the real-time program refinement calculus. - Ian J. Hayes (Sci. Comput. Program., 2007)

Probabilistic Choice in Refinement Algebra. - Larissa Meinicke; Ian J. Hayes (MPC, 2008)

Towards reasoning about teleo-reactive programs for robust real-time systems. - Ian J. Hayes (SERENE, 2008)

Reasoning about Loops in Total and General Correctness. - Steve Dunne; Ian J. Hayes; Andy Galloway (UTP, 2008)

Algebraic reasoning for probabilistic action systems and while-loops. - Larissa Meinicke; Ian J. Hayes (Acta Informatica, 2008)

Calculating modules in contextual logic program refinement. - Robert Colvin; Ian J. Hayes; Paul A. Strooper (Theory Pract. Log. Program., 2008)

Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation. - Brijesh Dongol; Ian J. Hayes (Australian Software Engineering Conference, 2009)

CSP with Hierarchical State. - Robert Colvin; Ian J. Hayes (IFM, 2009)

Dynamically Detecting Faults via Integrity Constraints. - Ian J. Hayes (Methods, Models and Tools for Fault Tolerance, 2009)

Invariants and Well-Foundedness in Program Algebra. - Ian J. Hayes (ICTAC, 2010)

Compositional Action System Derivation Using Enforced Properties. - Brijesh Dongol; Ian J. Hayes (MPC, 2010)

Unifying Theories of Programming That Distinguish Nontermination and Abort. - Ian J. Hayes; Steve Dunne; Larissa Meinicke (MPC, 2010)

Integrating Requirements: The Behavior Tree Philosophy. - Kirsten Winter; Ian J. Hayes; Robert Colvin (SEFM, 2010)

A timeband framework for modelling real-time systems. - Alan Burns 001; Ian J. Hayes (Real Time Syst., 2010)

Model-Driven Web Form Validation with UML and OCL. - Eban Escott; Paul A. Strooper; Paul King; Ian J. Hayes (ICWE Workshops, 2011)

Approximating Idealised Real-Time Specifications Using Time Bands. - Brijesh Dongol; Ian J. Hayes (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Structural operational semantics through context-dependent behaviour. - Robert Colvin; Ian J. Hayes (J. Log. Algebraic Methods Program., 2011)

A semantics for Behavior Trees using CSP with specification commands. - Robert Colvin; Ian J. Hayes (Sci. Comput. Program., 2011)

Towards an Algebra for Real-Time Programs. - Brijesh Dongol; Ian J. Hayes; Larissa Meinicke; Kim Solin (RAMiCS, 2012)

Integrated Operational Semantics: Small-Step, Big-Step and Multi-step. - Ian J. Hayes; Robert Colvin (ABZ, 2012)

Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. - Brijesh Dongol; Ian J. Hayes (IFM, 2012)

Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. - Brijesh Dongol; Ian J. Hayes (MPC, 2012)

Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. - Brijesh Dongol; John Derrick; Ian J. Hayes (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions. - Ian J. Hayes (FTSCS, 2013)

Path-Sensitive Data Flow Analysis Simplified. - Kirsten Winter; Chenyi Zhang 001; Ian J. Hayes; Nathan Keynes; Cristina Cifuentes; Lian Li (ICFEM, 2013)

Visuocode: A software development environment that supports spatial navigation and composition. - Daniel R. Bradley; Ian J. Hayes (VISSOFT, 2013)

Comparing Degrees of Non-Determinism in Expression Evaluation. - Ian J. Hayes; Alan Burns 001; Brijesh Dongol; Cliff B. Jones (Comput. J., 2013)

Deriving real-time action systems in a sampling logic. - Brijesh Dongol; Ian J. Hayes (Sci. Comput. Program., 2013)

Linking Unifying Theories of Program refinement. - Ian J. Hayes; Steve Dunne; Larissa Meinicke (Sci. Comput. Program., 2013)

Invariants, Well-Founded Statements and Real-Time Program Algebra. - Ian J. Hayes; Larissa Meinicke (FM, 2014)

Convolution, Separation and Concurrency. - Brijesh Dongol; Ian J. Hayes; Georg Struth (CoRR, 2014)

Reasoning about goal-directed real-time teleo-reactive programs. - Brijesh Dongol; Ian J. Hayes; Peter J. Robinson 001 (Formal Aspects Comput., 2014)

Deriving real-time action systems with multiple time bands using algebraic reasoning. - Brijesh Dongol; Ian J. Hayes; John Derrick (Sci. Comput. Program., 2014)

Balancing expressiveness in formal approaches to concurrency. - Cliff B. Jones; Ian J. Hayes; Robert J. Colvin (Formal Aspects Comput., 2015)

An Algebra of Synchronous Atomic Steps. - Ian J. Hayes; Robert J. Colvin; Larissa A. Meinicke; Kirsten Winter; Andrius Velykis (FM, 2016)

Concurrent Refinement Algebra and Rely Quotients. - Julian Fell; Ian J. Hayes; Andrius Velykis (Arch. Formal Proofs, 2016)

Generalised rely-guarantee concurrency: an algebraic foundation. - Ian J. Hayes (Formal Aspects Comput., 2016)

Possible values: Exploring a concept for concurrency. - Cliff B. Jones; Ian J. Hayes (J. Log. Algebraic Methods Program., 2016)

Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. - Brijesh Dongol; Ian J. Hayes; Georg Struth (ACM Trans. Comput. Log., 2016)

Capabilities for Java: Secure Access to Resources. - Ian J. Hayes; Xi Wu 005; Larissa A. Meinicke (APLAS, 2017)

A Guide to Rely/Guarantee Thinking. - Ian J. Hayes; Cliff B. Jones (SETSS, 2017)

Partial Semigroups and Convolution Algebras. - Brijesh Dongol; Victor B. F. Gomes; Ian J. Hayes; Georg Struth (Arch. Formal Proofs, 2017)

Relational Convolution, Generalised Modalities and Incidence Algebras. - Brijesh Dongol; Ian J. Hayes; Georg Struth (CoRR, 2017)

Designing a semantic model for a wide-spectrum language with concurrency. - Robert J. Colvin; Ian J. Hayes; Larissa A. Meinicke (Formal Aspects Comput., 2017)

Encoding Fairness in a Synchronous Concurrent Program Algebra. - Ian J. Hayes; Larissa A. Meinicke (FM, 2018)

Engineering a Theory of Concurrent Programming. - Ian J. Hayes (ICFEM, 2018)

Type Capabilities for Object-Oriented Programming Languages. - Xi Wu 005; Yi Lu 003; Patrick A. Meiring; Ian J. Hayes; Larissa A. Meinicke (ICFEM, 2018)

Encoding fairness in a synchronous concurrent program algebra: extended version with proofs. - Ian J. Hayes; Larissa A. Meinicke (CoRR, 2018)

Some Challenges of Specifying Concurrent Program Components. - Ian J. Hayes (Refine@FM, 2018)

Cylindric Kleene Lattices for Program Construction. - Brijesh Dongol; Ian J. Hayes; Larissa Meinicke; Georg Struth (MPC, 2019)

Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges. - Ian J. Hayes; Larissa A. Meinicke (UTP, 2019)

Handling localisation in rely/guarantee concurrency: An algebraic approach. - Larissa A. Meinicke; Ian J. Hayes (CoRR, 2019)

A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. - Ian J. Hayes; Larissa A. Meinicke; Kirsten Winter; Robert J. Colvin (Formal Aspects Comput., 2019)

Deriving Specifications of Control Programs for Cyber Physical Systems. - Alan Burns 001; Ian J. Hayes; Cliff B. Jones (Comput. J., 2020)

Software Specification. - Ian J. Hayes; Steve King 001 (Theories of Programming, 2021)

A Formal Semantics of the GraalVM Intermediate Representation. - Brae J. Webb; Mark Utting; Ian J. Hayes (ATVA, 2021)

Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style. - Ian J. Hayes; Larissa A. Meinicke; Patrick A. Meiring (CoRR, 2021)

Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras. - Brijesh Dongol; Ian J. Hayes; Georg Struth (Log. Methods Comput. Sci., 2021)

Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper). - Mark Utting; Brae J. Webb; Ian J. Hayes (CoRR, 2022)

Contextuality in Distributed Systems. - Nasos Evangelou-Oost; Callum Bannister; Ian J. Hayes (RAMiCS, 2023)

Specifying and Reasoning About Shared-Variable Concurrency. - Ian J. Hayes; Cliff B. Jones; Larissa A. Meinicke (Theories of Programming and Formal Methods, 2023)

Verifying Term Graph Optimizations using Isabelle/HOL. - Brae J. Webb; Ian J. Hayes; Mark Utting (CPP, 2023)

Trace Models of Concurrent Valuation Algebras. - Nasos Evangelou-Oost; Larissa Meinicke; Callum Bannister; Ian J. Hayes (ICFEM, 2023)

Verifying Compiler Optimisations - (Invited Paper). - Ian J. Hayes; Mark Utting; Brae J. Webb (ICFEM, 2023)

Using scylindric algebra to support local variables in rely/guarantee concurrency. - Larissa A. Meinicke; Ian J. Hayes (FormaliSE, 2023)

Differential Testing of a Verification Framework for Compiler Optimizations (Case Study). - Mark Utting; Brae J. Webb; Ian J. Hayes (FormaliSE, 2023)

Restructuring a Concurrent Refinement Algebra. - Ian J. Hayes; Larissa A. Meinicke; Nasos Evangelou-Oost (RAMiCS, 2024)

Reasoning about distributive laws in a concurrent refinement algebra. - Larissa A. Meinicke; Ian J. Hayes (CoRR, 2024)

Data reification in a concurrent rely-guarantee algebra. - Larissa A. Meinicke; Ian J. Hayes; Cliff B. Jones (CoRR, 2024)

Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures. - Robert J. Colvin; Ian J. Hayes; Scott Heiner; Peter Höfner; Larissa Meinicke; Roger C. Su (CoRR, 2024)

Handling expression evaluation under interference. - Ian J. Hayes; Cliff B. Jones; Larissa A. Meinicke (CoRR, 2024)

Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures. - Robert J. Colvin; Ian J. Hayes; Scott Heiner; Peter Höfner; Larissa Meinicke; Roger C. Su (The Practice of Formal Methods (I), 2024)

Reasoning About Distributive Laws in a Concurrent Refinement Algebra. - Larissa A. Meinicke; Ian J. Hayes (The Practice of Formal Methods (II), 2024)