


default search action
Ian J. Hayes
Person information
- affiliation: University of Queensland, Brisbane, Australia
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [c76]Ian J. Hayes
, Larissa A. Meinicke
, Nasos Evangelou-Oost
:
Restructuring a Concurrent Refinement Algebra. RAMiCS 2024: 135-155 - [i22]Larissa A. Meinicke, Ian J. Hayes:
Reasoning about distributive laws in a concurrent refinement algebra. CoRR abs/2403.13425 (2024) - [i21]Larissa A. Meinicke, Ian J. Hayes, Cliff B. Jones:
Data reification in a concurrent rely-guarantee algebra. CoRR abs/2405.05546 (2024) - [i20]Ian J. Hayes, Larissa A. Meinicke, Nasos Evangelou-Oost:
Restructuring a concurrent refinement algebra. CoRR abs/2405.05690 (2024) - [i19]Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su:
Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures. CoRR abs/2407.20559 (2024) - [i18]Ian J. Hayes, Cliff B. Jones, Larissa A. Meinicke:
Handling expression evaluation under interference. CoRR abs/2409.07741 (2024) - 2023
- [c75]Nasos Evangelou-Oost
, Callum Bannister
, Ian J. Hayes
:
Contextuality in Distributed Systems. RAMiCS 2023: 52-68 - [c74]Ian J. Hayes
, Cliff B. Jones
, Larissa A. Meinicke
:
Specifying and Reasoning About Shared-Variable Concurrency. Theories of Programming and Formal Methods 2023: 110-135 - [c73]Brae J. Webb
, Ian J. Hayes, Mark Utting
:
Verifying Term Graph Optimizations using Isabelle/HOL. CPP 2023: 320-333 - [c72]Ian J. Hayes, Mark Utting
, Brae J. Webb
:
Verifying Compiler Optimisations - (Invited Paper). ICFEM 2023: 3-8 - [c71]Nasos Evangelou-Oost
, Larissa Meinicke
, Callum Bannister
, Ian J. Hayes
:
Trace Models of Concurrent Valuation Algebras. ICFEM 2023: 118-136 - [c70]Mark Utting
, Brae J. Webb
, Ian J. Hayes:
Differential Testing of a Verification Framework for Compiler Optimizations (Case Study). FormaliSE 2023: 66-75 - [c69]Larissa A. Meinicke
, Ian J. Hayes:
Using scylindric algebra to support local variables in rely/guarantee concurrency. FormaliSE 2023: 108-119 - [i17]Nasos Evangelou-Oost, Callum Bannister, Larissa Meinicke, Ian J. Hayes:
Trace models of concurrent valuation algebras. CoRR abs/2305.18017 (2023) - 2022
- [i16]Nasos Evangelou-Oost, Callum Bannister, Ian J. Hayes:
Contextuality in distributed systems. CoRR abs/2210.09476 (2022) - [i15]Mark Utting, Brae J. Webb, Ian J. Hayes:
Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper). CoRR abs/2212.01748 (2022) - [i14]Brae J. Webb, Ian J. Hayes, Mark Utting:
Verifying term graph optimizations using Isabelle/HOL. CoRR abs/2212.06956 (2022) - 2021
- [j45]Brijesh Dongol, Ian J. Hayes, Georg Struth:
Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras. Log. Methods Comput. Sci. 17(1) (2021) - [c68]Brae J. Webb
, Mark Utting
, Ian J. Hayes
:
A Formal Semantics of the GraalVM Intermediate Representation. ATVA 2021: 111-126 - [p3]Ian J. Hayes, Steve King:
Software Specification. Theories of Programming 2021: 251-270 - [i13]Ian J. Hayes, Larissa A. Meinicke, Patrick A. Meiring:
Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style. CoRR abs/2103.15292 (2021) - [i12]Brae J. Webb
, Mark Utting, Ian J. Hayes:
A Formal Semantics of the GraalVM Intermediate Representation. CoRR abs/2107.01815 (2021) - 2020
- [j44]Alan Burns
, Ian J. Hayes
, Cliff B. Jones
:
Deriving Specifications of Control Programs for Cyber Physical Systems. Comput. J. 63(5): 774-790 (2020)
2010 – 2019
- 2019
- [j43]Ian J. Hayes
, Larissa A. Meinicke
, Kirsten Winter, Robert J. Colvin:
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects Comput. 31(2): 133-163 (2019) - [c67]Brijesh Dongol
, Ian J. Hayes
, Larissa Meinicke
, Georg Struth:
Cylindric Kleene Lattices for Program Construction. MPC 2019: 197-225 - [c66]Ian J. Hayes
, Larissa A. Meinicke
:
Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges. UTP 2019: 176-197 - [i11]Larissa A. Meinicke, Ian J. Hayes:
Handling localisation in rely/guarantee concurrency: An algebraic approach. CoRR abs/1907.04005 (2019) - 2018
- [c65]Ian J. Hayes, Larissa A. Meinicke
:
Encoding Fairness in a Synchronous Concurrent Program Algebra. FM 2018: 222-239 - [c64]Ian J. Hayes:
Engineering a Theory of Concurrent Programming. ICFEM 2018: 3-18 - [c63]Xi Wu
, Yi Lu
, Patrick A. Meiring
, Ian J. Hayes
, Larissa A. Meinicke
:
Type Capabilities for Object-Oriented Programming Languages. ICFEM 2018: 215-230 - [c62]Ian J. Hayes:
Some Challenges of Specifying Concurrent Program Components. Refine@FM 2018: 10-22 - [i10]Ian J. Hayes, Larissa A. Meinicke:
Encoding fairness in a synchronous concurrent program algebra: extended version with proofs. CoRR abs/1805.01681 (2018) - 2017
- [j42]Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes, Georg Struth:
Partial Semigroups and Convolution Algebras. Arch. Formal Proofs 2017 (2017) - [j41]Robert J. Colvin, Ian J. Hayes
, Larissa A. Meinicke
:
Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects Comput. 29(5): 853-875 (2017) - [c61]Ian J. Hayes, Xi Wu, Larissa A. Meinicke
:
Capabilities for Java: Secure Access to Resources. APLAS 2017: 67-84 - [c60]Ian J. Hayes
, Cliff B. Jones
:
A Guide to Rely/Guarantee Thinking. SETSS 2017: 1-38 - [i9]Brijesh Dongol
, Ian J. Hayes, Georg Struth:
Relational Convolution, Generalised Modalities and Incidence Algebras. CoRR abs/1702.04603 (2017) - [i8]Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, Robert J. Colvin:
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. CoRR abs/1710.03352 (2017) - 2016
- [j40]Julian Fell, Ian J. Hayes, Andrius Velykis:
Concurrent Refinement Algebra and Rely Quotients. Arch. Formal Proofs 2016 (2016) - [j39]Ian J. Hayes
:
Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects Comput. 28(6): 1057-1078 (2016) - [j38]Cliff B. Jones
, Ian J. Hayes
:
Possible values: Exploring a concept for concurrency. J. Log. Algebraic Methods Program. 85(5): 972-984 (2016) - [j37]Brijesh Dongol
, Ian J. Hayes, Georg Struth:
Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. ACM Trans. Comput. Log. 17(3): 15 (2016) - [c59]Ian J. Hayes, Robert J. Colvin, Larissa A. Meinicke
, Kirsten Winter, Andrius Velykis:
An Algebra of Synchronous Atomic Steps. FM 2016: 352-369 - [i7]Cliff B. Jones, Ian J. Hayes:
Possible values: exploring a concept for concurrency. CoRR abs/1601.02132 (2016) - [i6]Ian J. Hayes:
Generalised rely-guarantee concurrency: An algebraic foundation. CoRR abs/1603.01776 (2016) - [i5]Ian J. Hayes, Robert Colvin, Larissa Meinicke, Kirsten Winter, Andrius Velykis:
An algebra of synchronous atomic steps. CoRR abs/1609.00118 (2016) - [i4]Robert J. Colvin, Ian J. Hayes, Larissa A. Meinicke:
Designing a semantic model for a wide-spectrum language with concurrency. CoRR abs/1609.00195 (2016) - 2015
- [j36]Cliff B. Jones
, Ian J. Hayes
, Robert J. Colvin:
Balancing expressiveness in formal approaches to concurrency. Formal Aspects Comput. 27(3): 475-497 (2015) - 2014
- [j35]Brijesh Dongol
, Ian J. Hayes
, Peter J. Robinson:
Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects Comput. 26(3): 563-589 (2014) - [j34]Brijesh Dongol
, Ian J. Hayes
, John Derrick
:
Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program. 85: 137-165 (2014) - [c58]Ian J. Hayes
, Larissa Meinicke
:
Invariants, Well-Founded Statements and Real-Time Program Algebra. FM 2014: 318-334 - [i3]Brijesh Dongol, Ian J. Hayes, Georg Struth:
Convolution, Separation and Concurrency. CoRR abs/1410.4235 (2014) - 2013
- [j33]Ian J. Hayes
, Alan Burns, Brijesh Dongol
, Cliff B. Jones
:
Comparing Degrees of Non-Determinism in Expression Evaluation. Comput. J. 56(6): 741-755 (2013) - [j32]Brijesh Dongol
, Ian J. Hayes
:
Deriving real-time action systems in a sampling logic. Sci. Comput. Program. 78(11): 2047-2063 (2013) - [j31]Ian J. Hayes
, Steve Dunne, Larissa Meinicke
:
Linking Unifying Theories of Program refinement. Sci. Comput. Program. 78(11): 2086-2107 (2013) - [c57]Ian J. Hayes
:
Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions. FTSCS 2013: 1-2 - [c56]Kirsten Winter, Chenyi Zhang
, Ian J. Hayes
, Nathan Keynes, Cristina Cifuentes, Lian Li:
Path-Sensitive Data Flow Analysis Simplified. ICFEM 2013: 415-430 - [c55]Daniel R. Bradley, Ian J. Hayes
:
Visuocode: A software development environment that supports spatial navigation and composition. VISSOFT 2013: 1-4 - 2012
- [j30]Brijesh Dongol, John Derrick, Ian J. Hayes:
Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 53 (2012) - [c54]Brijesh Dongol
, Ian J. Hayes
, Larissa Meinicke
, Kim Solin:
Towards an Algebra for Real-Time Programs. RAMiCS 2012: 50-65 - [c53]Ian J. Hayes
, Robert Colvin
:
Integrated Operational Semantics: Small-Step, Big-Step and Multi-step. ABZ 2012: 21-35 - [c52]Brijesh Dongol
, Ian J. Hayes
:
Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. IFM 2012: 39-53 - [c51]Brijesh Dongol
, Ian J. Hayes
:
Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. MPC 2012: 102-131 - 2011
- [j29]Brijesh Dongol, Ian J. Hayes:
Approximating Idealised Real-Time Specifications Using Time Bands. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46 (2011) - [j28]Robert Colvin
, Ian J. Hayes
:
Structural operational semantics through context-dependent behaviour. J. Log. Algebraic Methods Program. 80(7): 392-426 (2011) - [j27]Robert Colvin
, Ian J. Hayes
:
A semantics for Behavior Trees using CSP with specification commands. Sci. Comput. Program. 76(10): 891-914 (2011) - [c50]Eban Escott, Paul A. Strooper
, Paul King, Ian J. Hayes
:
Model-Driven Web Form Validation with UML and OCL. ICWE Workshops 2011: 223-235 - 2010
- [j26]Alan Burns, Ian J. Hayes
:
A timeband framework for modelling real-time systems. Real Time Syst. 45(1-2): 106-142 (2010) - [c49]Ian J. Hayes
:
Invariants and Well-Foundedness in Program Algebra. ICTAC 2010: 1-14 - [c48]Brijesh Dongol
, Ian J. Hayes
:
Compositional Action System Derivation Using Enforced Properties. MPC 2010: 119-139 - [c47]Ian J. Hayes
, Steve Dunne, Larissa Meinicke:
Unifying Theories of Programming That Distinguish Nontermination and Abort. MPC 2010: 178-194 - [c46]Kirsten Winter, Ian J. Hayes
, Robert Colvin:
Integrating Requirements: The Behavior Tree Philosophy. SEFM 2010: 41-50
2000 – 2009
- 2009
- [c45]Brijesh Dongol
, Ian J. Hayes
:
Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation. Australian Software Engineering Conference 2009: 3-12 - [c44]Robert Colvin, Ian J. Hayes
:
CSP with Hierarchical State. IFM 2009: 118-135 - [p2]Ian J. Hayes
:
Dynamically Detecting Faults via Integrity Constraints. Methods, Models and Tools for Fault Tolerance 2009: 85-103 - 2008
- [j25]Larissa Meinicke
, Ian J. Hayes
:
Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica 45(5): 321-382 (2008) - [j24]Robert Colvin
, Ian J. Hayes
, Paul A. Strooper
:
Calculating modules in contextual logic program refinement. Theory Pract. Log. Program. 8(1): 1-31 (2008) - [c43]Larissa Meinicke
, Ian J. Hayes
:
Probabilistic Choice in Refinement Algebra. MPC 2008: 243-267 - [c42]Ian J. Hayes
:
Towards reasoning about teleo-reactive programs for robust real-time systems. SERENE 2008: 87-94 - [c41]Steve Dunne, Ian J. Hayes
, Andy Galloway:
Reasoning about Loops in Total and General Correctness. UTP 2008: 62-81 - 2007
- [j23]Ian J. Hayes
:
Procedures and parameters in the real-time program refinement calculus. Sci. Comput. Program. 64(3): 286-311 (2007) - [c40]Cliff B. Jones
, Ian J. Hayes
, Michael A. Jackson:
Deriving Specifications for Systems That Are Connected to the Physical World. Formal Methods and Hybrid Real-Time Systems 2007: 364-390 - 2006
- [c39]Larissa Meinicke
, Ian J. Hayes
:
Reasoning Algebraically About Probabilistic Loops. ICFEM 2006: 380-399 - [c38]Larissa Meinicke
, Ian J. Hayes
:
Continuous Action System Refinement. MPC 2006: 316-337 - [c37]Ian J. Hayes
:
Termination of Real-Time Programs: Definitely, Definitely Not, or Maybe. UTP 2006: 141-154 - [i2]Robert Colvin, Ian J. Hayes, Paul A. Strooper:
Calculating modules in contextual logic program refinement. CoRR abs/cs/0608110 (2006) - 2005
- [j22]Karl Lermer, Colin J. Fidge
, Ian J. Hayes
:
A theory for execution-time derivation in real-time programs. Theor. Comput. Sci. 346(1): 3-27 (2005) - [c36]Erica Glynn, Ian J. Hayes, Anthony MacDonald:
Integration of generic program analysis tools into a software development environment. ACSC 2005: 249-258 - [e1]John S. Fitzgerald, Ian J. Hayes
, Andrzej Tarlecki:
FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings. Lecture Notes in Computer Science 3582, Springer 2005, ISBN 3-540-27882-6 [contents] - 2004
- [c35]Ian J. Hayes
:
Towards Platform-Independent Real-Time Systems. Australian Software Engineering Conference 2004: 192-201 - [c34]Cameron Smith, Kirsten Winter, Ian J. Hayes, R. Geoff Dromey, Peter A. Lindsay, David A. Carrington:
An Environment for Building a System out of its Requirements. ASE 2004: 398-399 - [p1]Robert Colvin, Lindsay Groves, Ian J. Hayes
, David Hemer, Ray Nickson, Paul A. Strooper:
Developing Logic Programs from Specifications Using Stepwise Refinement. Program Development in Computational Logic 2004: 66-89 - 2003
- [j21]Karl Lermer, Colin J. Fidge
, Ian J. Hayes
:
Linear Approximation of Execution-Time Constraints. Formal Aspects Comput. 15(4): 319-348 (2003) - [c33]Ian J. Hayes
, Michael A. Jackson, Cliff B. Jones
:
Determining the Specification of a Control System from That of Its Environment. FME 2003: 154-169 - [c32]Ian J. Hayes
:
Programs as Paths: An Approach to Timing Constraint Analysis. ICFEM 2003: 1-15 - [c31]Sibylle Peuker, Ian J. Hayes
:
Reasoning about Deadlines in Concurrent Real-Time Programs. IPDPS 2003: 237 - [c30]Karl Lermer, Colin J. Fidge
, Ian J. Hayes
:
Formal Semantics for Program Paths. CATS 2003: 58-81 - 2002
- [j20]Graeme Smith
, Ian J. Hayes
:
An Introduction to Real-Time Object-Z. Formal Aspects Comput. 13(2): 128-141 (2002) - [j19]Ian J. Hayes
:
Reasoning about real-time repetitions: terminating and nonterminating. Sci. Comput. Program. 43(2-3): 161-192 (2002) - [j18]Ian J. Hayes
, Robert Colvin
, David Hemer, Paul A. Strooper
, Ray Nickson:
A refinement calculus for logic programs. Theory Pract. Log. Program. 2(4-5): 425-460 (2002) - [c29]Robert Colvin, Ian J. Hayes, David Hemer, Paul A. Strooper:
Translating Refined Logic Programs to Mercury. ACSC 2002: 33-40 - [c28]Ian J. Hayes
:
The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming. ICATPN 2002: 44-58 - [c27]Jamie Shield, Ian J. Hayes:
Refining Object-Oriented Invariants and Dynamic Constraints. APSEC 2002: 52- - [c26]Sibylle Peuker, Ian J. Hayes
:
Towards a Refinement Calculus for Concurrent Real-Time Programs. ICFEM 2002: 335-346 - [c25]Robert Colvin
, Ian J. Hayes
, David Hemer, Paul A. Strooper:
Refinement of Higher-Order Logic Programs. LOPSTR 2002: 126-143 - [c24]Ian J. Hayes
:
Reasoning about Timeouts. MPC 2002: 94-116 - [c23]David Hemer, Ian J. Hayes
, Paul A. Strooper
, Robert Colvin:
Don't Care Non-determinism in Logic Program Refinement. CATS 2002: 101-121 - [i1]Ian J. Hayes, Robert Colvin, David Hemer, Paul A. Strooper, Ray Nickson:
A Refinement Calculus for Logic Programs. CoRR cs.SE/0202002 (2002) - 2001
- [j17]Ian J. Hayes
, Mark Utting
:
A sequential real-time refinement calculus. Acta Informatica 37(6): 385-448 (2001) - [j16]Ian J. Hayes
, Colin J. Fidge
, Karl Lermer:
Semantic characterisation of dead control-flow paths. IEE Proc. Softw. 148(6): 175-186 (2001) - [c22]David Hemer, Ian J. Hayes
, Paul A. Strooper:
Refinement Calculus for Logic Programming in Isabelle/HOL. TPHOLs 2001: 249-264 - [c21]Jamie Shield, Ian J. Hayes
, David A. Carrington:
Using Theory Interpretation to Mechanise the Reals in a Theorem Prover. CATS 2001: 266-281 - 2000
- [c20]Robert Colvin, Ian J. Hayes, Paul A. Strooper:
Refining Logic Programs Using Types. ACSC 2000: 43-50 - [c19]Ian J. Hayes
:
Reasoning about real-time programs using idle-invariant assertions. APSEC 2000: 16-23 - [c18]Ian J. Hayes
:
Real-Time Program Refinement Using Auxiliary Variables. FTRTFT 2000: 170-184 - [c17]Graeme Smith
, Ian J. Hayes
:
Structuring Real-Time Object-Z Specifications. IFM 2000: 97-115 - [c16]Robert Colvin, Ian J. Hayes, Paul A. Strooper:
Modular Logic Program Refinement. LOPSTR 2000 - [c15]Robert Colvin
, Ian J. Hayes
, Paul A. Strooper:
A Technique for Modular Logic Program Refinement. LOPSTR (LNCS 2042: Selected Papers) 2000: 38-56 - [c14]Ian J. Hayes
:
Reasoning about Non-terminating Loops Using Deadline Commands. MPC 2000: 60-79
1990 – 1999
- 1999
- [j15]Colin J. Fidge
, Ian J. Hayes, Geoffrey Watson:
The deadline command. IEE Proc. Softw. 146(2): 104-111 (1999) - [c13]Graeme Smith
, Ian J. Hayes
:
Towards Real-Time Object-Z. IFM 1999: 49-65 - 1998
- [j14]David A. Carrington, Ian J. Hayes
, Ray Nickson, Geoffrey Watson, Jim Welsh:
A Program Refinement Tool. Formal Aspects Comput. 10(2): 97-124 (1998) - [j13]Ian J. Hayes
:
Expressive Power of Specification Languages. Formal Aspects Comput. 10(2): 187-192 (1998) - [c12]Colin J. Fidge
, Ian J. Hayes, Brendan P. Mahony:
Defining Differentiation and Integration in Z. ICFEM 1998: 64-75 - [c11]