Ian J. Hayes - RankMe

150 papers A* 1A 1B 22C 20Journal 68Unranked 33

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Reasoning about concurrent loops and recursion with rely-guarantee rules. CoRR Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones
2024	J	`jnl`	Data reification in a concurrent rely-guarantee algebra. CoRR Larissa A. Meinicke, Ian J. Hayes, Cliff B. Jones
2024	J	`jnl`	Handling expression evaluation under interference. CoRR Ian J. Hayes, Cliff B. Jones, Larissa A. Meinicke
2024	J	`jnl`	Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures. CoRR Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su
2024	—	`ch.`	Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures. The Practice of Formal Methods (I) Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su
2024	—	`ch.`	Reasoning About Distributive Laws in a Concurrent Refinement Algebra. The Practice of Formal Methods (II) Larissa A. Meinicke, Ian J. Hayes
2024	J	`jnl`	Reasoning about distributive laws in a concurrent refinement algebra. CoRR Larissa A. Meinicke, Ian J. Hayes
2024	C	`conf`	Restructuring a Concurrent Refinement Algebra. RAMiCS Ian J. Hayes, Larissa A. Meinicke, Nasos Evangelou-Oost
2024	J	`jnl`	Restructuring a concurrent refinement algebra. CoRR Ian J. Hayes, Larissa A. Meinicke, Nasos Evangelou-Oost
2023	C	`conf`	Contextuality in Distributed Systems. RAMiCS Nasos Evangelou-Oost, Callum Bannister, Ian J. Hayes
2023	—	`conf`	Differential Testing of a Verification Framework for Compiler Optimizations (Case Study). FormaliSE Mark Utting, Brae J. Webb, Ian J. Hayes
2023	—	`conf`	Specifying and Reasoning About Shared-Variable Concurrency. Theories of Programming and Formal Methods Ian J. Hayes, Cliff B. Jones, Larissa A. Meinicke
2023	C	`conf`	Trace Models of Concurrent Valuation Algebras. ICFEM Nasos Evangelou-Oost, Larissa Meinicke, Callum Bannister, Ian J. Hayes
2023	J	`jnl`	Trace models of concurrent valuation algebras. CoRR Nasos Evangelou-Oost, Callum Bannister, Larissa Meinicke, Ian J. Hayes
2023	—	`conf`	Using scylindric algebra to support local variables in rely/guarantee concurrency. FormaliSE Larissa A. Meinicke, Ian J. Hayes
2023	C	`conf`	Verifying Compiler Optimisations - (Invited Paper). ICFEM Ian J. Hayes, Mark Utting, Brae J. Webb
2023	B	`conf`	Verifying Term Graph Optimizations using Isabelle/HOL. CPP Brae J. Webb, Ian J. Hayes, Mark Utting
2022	J	`jnl`	Contextuality in distributed systems. CoRR Nasos Evangelou-Oost, Callum Bannister, Ian J. Hayes
2022	J	`jnl`	Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper). CoRR Mark Utting, Brae J. Webb, Ian J. Hayes
2022	J	`jnl`	Verifying term graph optimizations using Isabelle/HOL. CoRR Brae J. Webb, Ian J. Hayes, Mark Utting
2021	B	`conf`	A Formal Semantics of the GraalVM Intermediate Representation. ATVA Brae J. Webb, Mark Utting, Ian J. Hayes
2021	J	`jnl`	A Formal Semantics of the GraalVM Intermediate Representation. CoRR Brae J. Webb, Mark Utting, Ian J. Hayes
2021	J	`jnl`	Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras. Log. Methods Comput. Sci. Brijesh Dongol, Ian J. Hayes, Georg Struth
2021	J	`jnl`	Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style. CoRR Ian J. Hayes, Larissa A. Meinicke, Patrick A. Meiring
2021	—	`ch.`	Software Specification. Theories of Programming Ian J. Hayes, Steve King
2020	J	`jnl`	Deriving Specifications of Control Programs for Cyber Physical Systems. Comput. J. Alan Burns, Ian J. Hayes, Cliff B. Jones
2019	J	`jnl`	A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. Formal Aspects Comput. Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, Robert J. Colvin
2019	B	`conf`	Cylindric Kleene Lattices for Program Construction. MPC Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth
2019	—	`conf`	Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges. UTP Ian J. Hayes, Larissa A. Meinicke
2019	J	`jnl`	Handling localisation in rely/guarantee concurrency: An algebraic approach. CoRR Larissa A. Meinicke, Ian J. Hayes
2018	B	`conf`	Encoding Fairness in a Synchronous Concurrent Program Algebra. FM Ian J. Hayes, Larissa A. Meinicke
2018	J	`jnl`	Encoding fairness in a synchronous concurrent program algebra: extended version with proofs. CoRR Ian J. Hayes, Larissa A. Meinicke
2018	C	`conf`	Engineering a Theory of Concurrent Programming. ICFEM Ian J. Hayes
2018	—	`conf`	Some Challenges of Specifying Concurrent Program Components. Refine@FM Ian J. Hayes
2018	C	`conf`	Type Capabilities for Object-Oriented Programming Languages. ICFEM Xi Wu, Yi Lu, Patrick A. Meiring, Ian J. Hayes, Larissa A. Meinicke
2017	—	`conf`	A Guide to Rely/Guarantee Thinking. SETSS Ian J. Hayes, Cliff B. Jones
2017	J	`jnl`	A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. CoRR Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, Robert J. Colvin
2017	B	`conf`	Capabilities for Java: Secure Access to Resources. APLAS Ian J. Hayes, Xi Wu, Larissa A. Meinicke
2017	J	`jnl`	Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects Comput. Robert J. Colvin, Ian J. Hayes, Larissa A. Meinicke
2017	J	`jnl`	Partial Semigroups and Convolution Algebras. Arch. Formal Proofs Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes, Georg Struth
2017	J	`jnl`	Relational Convolution, Generalised Modalities and Incidence Algebras. CoRR Brijesh Dongol, Ian J. Hayes, Georg Struth
2016	B	`conf`	An Algebra of Synchronous Atomic Steps. FM Ian J. Hayes, Robert J. Colvin, Larissa A. Meinicke, Kirsten Winter, Andrius Velykis
2016	J	`jnl`	An algebra of synchronous atomic steps. CoRR Ian J. Hayes, Robert Colvin, Larissa Meinicke, Kirsten Winter, Andrius Velykis
2016	J	`jnl`	Concurrent Refinement Algebra and Rely Quotients. Arch. Formal Proofs Julian Fell, Ian J. Hayes, Andrius Velykis
2016	J	`jnl`	Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency. ACM Trans. Comput. Log. Brijesh Dongol, Ian J. Hayes, Georg Struth
2016	J	`jnl`	Designing a semantic model for a wide-spectrum language with concurrency. CoRR Robert J. Colvin, Ian J. Hayes, Larissa A. Meinicke
2016	J	`jnl`	Generalised rely-guarantee concurrency: An algebraic foundation. CoRR Ian J. Hayes
2016	J	`jnl`	Generalised rely-guarantee concurrency: an algebraic foundation. Formal Aspects Comput. Ian J. Hayes
2016	J	`jnl`	Possible values: Exploring a concept for concurrency. J. Log. Algebraic Methods Program. Cliff B. Jones, Ian J. Hayes
2016	J	`jnl`	Possible values: exploring a concept for concurrency. CoRR Cliff B. Jones, Ian J. Hayes
2015	J	`jnl`	Balancing expressiveness in formal approaches to concurrency. Formal Aspects Comput. Cliff B. Jones, Ian J. Hayes, Robert J. Colvin
2014	J	`jnl`	Convolution, Separation and Concurrency. CoRR Brijesh Dongol, Ian J. Hayes, Georg Struth
2014	J	`jnl`	Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program. Brijesh Dongol, Ian J. Hayes, John Derrick
2014	B	`conf`	Invariants, Well-Founded Statements and Real-Time Program Algebra. FM Ian J. Hayes, Larissa Meinicke
2014	J	`jnl`	Reasoning about goal-directed real-time teleo-reactive programs. Formal Aspects Comput. Brijesh Dongol, Ian J. Hayes, Peter J. Robinson
2013	J	`jnl`	Comparing Degrees of Non-Determinism in Expression Evaluation. Comput. J. Ian J. Hayes, Alan Burns, Brijesh Dongol, Cliff B. Jones
2013	J	`jnl`	Deriving real-time action systems in a sampling logic. Sci. Comput. Program. Brijesh Dongol, Ian J. Hayes
2013	J	`jnl`	Linking Unifying Theories of Program refinement. Sci. Comput. Program. Ian J. Hayes, Steve Dunne, Larissa Meinicke
2013	C	`conf`	Path-Sensitive Data Flow Analysis Simplified. ICFEM Kirsten Winter, Chenyi Zhang, Ian J. Hayes, Nathan Keynes, Cristina Cifuentes, Lian Li
2013	—	`conf`	Towards Structuring System Specifications with Time Bands Using Layers of Rely-Guarantee Conditions. FTSCS Ian J. Hayes
2013	B	`conf`	Visuocode: A software development environment that supports spatial navigation and composition. VISSOFT Daniel R. Bradley, Ian J. Hayes
2012	B	`conf`	Deriving Real-Time Action Systems Controllers from Multiscale System Specifications. MPC Brijesh Dongol, Ian J. Hayes
2012	J	`jnl`	Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Brijesh Dongol, John Derrick, Ian J. Hayes
2012	C	`conf`	Integrated Operational Semantics: Small-Step, Big-Step and Multi-step. ABZ Ian J. Hayes, Robert Colvin
2012	B	`conf`	Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands. IFM Brijesh Dongol, Ian J. Hayes
2012	C	`conf`	Towards an Algebra for Real-Time Programs. RAMiCS Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, Kim Solin
2011	J	`jnl`	A semantics for Behavior Trees using CSP with specification commands. Sci. Comput. Program. Robert Colvin, Ian J. Hayes
2011	J	`jnl`	Approximating Idealised Real-Time Specifications Using Time Bands. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. Brijesh Dongol, Ian J. Hayes
2011	—	`conf`	Model-Driven Web Form Validation with UML and OCL. ICWE Workshops Eban Escott, Paul A. Strooper, Paul King, Ian J. Hayes
2011	J	`jnl`	Structural operational semantics through context-dependent behaviour. J. Log. Algebraic Methods Program. Robert Colvin, Ian J. Hayes
2010	J	`jnl`	A timeband framework for modelling real-time systems. Real Time Syst. Alan Burns, Ian J. Hayes
2010	B	`conf`	Compositional Action System Derivation Using Enforced Properties. MPC Brijesh Dongol, Ian J. Hayes
2010	B	`conf`	Integrating Requirements: The Behavior Tree Philosophy. SEFM Kirsten Winter, Ian J. Hayes, Robert Colvin
2010	C	`conf`	Invariants and Well-Foundedness in Program Algebra. ICTAC Ian J. Hayes
2010	B	`conf`	Unifying Theories of Programming That Distinguish Nontermination and Abort. MPC Ian J. Hayes, Steve Dunne, Larissa Meinicke
2009	B	`conf`	CSP with Hierarchical State. IFM Robert Colvin, Ian J. Hayes
2009	—	`ch.`	Dynamically Detecting Faults via Integrity Constraints. Methods, Models and Tools for Fault Tolerance Ian J. Hayes
2009	—	`conf`	Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation. Australian Software Engineering Conference Brijesh Dongol, Ian J. Hayes
2008	J	`jnl`	Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica Larissa Meinicke, Ian J. Hayes
2008	J	`jnl`	Calculating modules in contextual logic program refinement. Theory Pract. Log. Program. Robert Colvin, Ian J. Hayes, Paul A. Strooper
2008	B	`conf`	Probabilistic Choice in Refinement Algebra. MPC Larissa Meinicke, Ian J. Hayes
2008	—	`conf`	Reasoning about Loops in Total and General Correctness. UTP Steve Dunne, Ian J. Hayes, Andy Galloway
2008	—	`conf`	Towards reasoning about teleo-reactive programs for robust real-time systems. SERENE Ian J. Hayes
2007	—	`conf`	Deriving Specifications for Systems That Are Connected to the Physical World. Formal Methods and Hybrid Real-Time Systems Cliff B. Jones, Ian J. Hayes, Michael A. Jackson
2007	J	`jnl`	Procedures and parameters in the real-time program refinement calculus. Sci. Comput. Program. Ian J. Hayes
2006	J	`jnl`	Calculating modules in contextual logic program refinement CoRR Robert Colvin, Ian J. Hayes, Paul A. Strooper
2006	B	`conf`	Continuous Action System Refinement. MPC Larissa Meinicke, Ian J. Hayes
2006	C	`conf`	Reasoning Algebraically About Probabilistic Loops. ICFEM Larissa Meinicke, Ian J. Hayes
2006	—	`conf`	Termination of Real-Time Programs: Definitely, Definitely Not, or Maybe. UTP Ian J. Hayes
2005	J	`jnl`	A theory for execution-time derivation in real-time programs. Theor. Comput. Sci. Karl Lermer, Colin J. Fidge, Ian J. Hayes
2005	B	`ed.`	FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings FM John S. Fitzgerald, Ian J. Hayes, Andrzej Tarlecki
2005	—	`conf`	Integration of generic program analysis tools into a software development environment. ACSC Erica Glynn, Ian J. Hayes, Anthony MacDonald
2004	A*	`conf`	An Environment for Building a System out of its Requirements. ASE Cameron Smith, Kirsten Winter, Ian J. Hayes, R. Geoff Dromey, Peter A. Lindsay, David A. Carrington
2004	—	`ch.`	Developing Logic Programs from Specifications Using Stepwise Refinement. Program Development in Computational Logic Robert Colvin, Lindsay Groves, Ian J. Hayes, David Hemer, Ray Nickson, Paul A. Strooper
2004	—	`conf`	Towards Platform-Independent Real-Time Systems. Australian Software Engineering Conference Ian J. Hayes
2003	—	`conf`	Determining the Specification of a Control System from That of Its Environment. FME Ian J. Hayes, Michael A. Jackson, Cliff B. Jones
2003	—	`conf`	Formal Semantics for Program Paths. CATS Karl Lermer, Colin J. Fidge, Ian J. Hayes
2003	J	`jnl`	Linear Approximation of Execution-Time Constraints. Formal Aspects Comput. Karl Lermer, Colin J. Fidge, Ian J. Hayes
2003	C	`conf`	Programs as Paths: An Approach to Timing Constraint Analysis. ICFEM Ian J. Hayes
2003	A	`conf`	Reasoning about Deadlines in Concurrent Real-Time Programs. IPDPS Sibylle Peuker, Ian J. Hayes
2002	J	`jnl`	A Refinement Calculus for Logic Programs CoRR Ian J. Hayes, Robert Colvin, David Hemer, Paul A. Strooper, Ray Nickson
2002	J	`jnl`	A refinement calculus for logic programs. Theory Pract. Log. Program. Ian J. Hayes, Robert Colvin, David Hemer, Paul A. Strooper, Ray Nickson
2002	J	`jnl`	An Introduction to Real-Time Object-Z. Formal Aspects Comput. Graeme Smith, Ian J. Hayes
2002	—	`conf`	Don't Care Non-determinism in Logic Program Refinement. CATS David Hemer, Ian J. Hayes, Paul A. Strooper, Robert Colvin
2002	B	`conf`	Reasoning about Timeouts. MPC Ian J. Hayes
2002	J	`jnl`	Reasoning about real-time repetitions: terminating and nonterminating. Sci. Comput. Program. Ian J. Hayes
2002	C	`conf`	Refinement of Higher-Order Logic Programs. LOPSTR Robert Colvin, Ian J. Hayes, David Hemer, Paul A. Strooper
2002	C	`conf`	Refining Object-Oriented Invariants and Dynamic Constraints. APSEC Jamie Shield, Ian J. Hayes
2002	—	`conf`	The Real-Time Refinement Calculus: A Foundation for Machine-Independent Real-Time Programming. ICATPN Ian J. Hayes
2002	C	`conf`	Towards a Refinement Calculus for Concurrent Real-Time Programs. ICFEM Sibylle Peuker, Ian J. Hayes
2002	—	`conf`	Translating Refined Logic Programs to Mercury. ACSC Robert Colvin, Ian J. Hayes, David Hemer, Paul A. Strooper
2001	J	`jnl`	A sequential real-time refinement calculus. Acta Informatica Ian J. Hayes, Mark Utting
2001	—	`conf`	Refinement Calculus for Logic Programming in Isabelle/HOL. TPHOLs David Hemer, Ian J. Hayes, Paul A. Strooper
2001	J	`jnl`	Semantic characterisation of dead control-flow paths. IEE Proc. Softw. Ian J. Hayes, Colin J. Fidge, Karl Lermer
2001	—	`conf`	Using Theory Interpretation to Mechanise the Reals in a Theorem Prover. CATS Jamie Shield, Ian J. Hayes, David A. Carrington
2000	—	`conf`	A Technique for Modular Logic Program Refinement. LOPSTR (LNCS 2042: Selected Papers) Robert Colvin, Ian J. Hayes, Paul A. Strooper
2000	C	`conf`	Modular Logic Program Refinement. LOPSTR Robert Colvin, Ian J. Hayes, Paul A. Strooper
2000	—	`conf`	Real-Time Program Refinement Using Auxiliary Variables. FTRTFT Ian J. Hayes
2000	B	`conf`	Reasoning about Non-terminating Loops Using Deadline Commands. MPC Ian J. Hayes
2000	C	`conf`	Reasoning about real-time programs using idle-invariant assertions. APSEC Ian J. Hayes
2000	—	`conf`	Refining Logic Programs Using Types. ACSC Robert Colvin, Ian J. Hayes, Paul A. Strooper
2000	B	`conf`	Structuring Real-Time Object-Z Specifications. IFM Graeme Smith, Ian J. Hayes
1999	J	`jnl`	The deadline command. IEE Proc. Softw. Colin J. Fidge, Ian J. Hayes, Geoffrey Watson
1999	B	`conf`	Towards Real-Time Object-Z. IFM Graeme Smith, Ian J. Hayes
1998	J	`jnl`	A Program Refinement Tool. Formal Aspects Comput. David A. Carrington, Ian J. Hayes, Ray Nickson, Geoffrey Watson, Jim Welsh
1998	B	`conf`	A Set-Theoretic Model for Real-Time Specification and Reasoning. MPC Colin J. Fidge, Ian J. Hayes, Andrew P. Martin, Axel Wabenhorst
1998	—	`conf`	Deadlines are termination. PROCOMET Ian J. Hayes, Mark Utting
1998	C	`conf`	Defining Differentiation and Integration in Z. ICFEM Colin J. Fidge, Ian J. Hayes, Brendan P. Mahony
1998	J	`jnl`	Expressive Power of Specification Languages. Formal Aspects Comput. Ian J. Hayes
1997	J	`jnl`	Supporting Contexts in Program Refinement. Sci. Comput. Program. Ray Nickson, Ian J. Hayes
1996	—	`conf`	Integrating Real-Time Scheduling Theory and Program Refinement. FME Colin J. Fidge, Mark Utting, Peter Kearney, Ian J. Hayes
1996	C	`conf`	Refining Specifications to Logic Programs. LOPSTR Ian J. Hayes, R. G. Nickson, Paul A. Strooper
1996	J	`jnl`	Supporting Module Reuse in Refinement. Sci. Comput. Program. Ian J. Hayes
1995	—	`conf`	A Formal Semantics for a Language with Type Extension. ZUM Peter Bancroft, Ian J. Hayes
1995	C	`conf`	Are Formal Methods Relevant? APSEC Ian J. Hayes, Keijiro Araki, David J. Duke, Val E. Veraart
1995	J	`jnl`	Specification by Interface Separation. Formal Aspects Comput. Ian J. Hayes, Jeff W. Sanders
1995	J	`jnl`	Using Units of Measurement in Formal Specifications. Formal Aspects Comput. Ian J. Hayes, Brendan P. Mahony
1994	J	`jnl`	Understanding the differences between VDM and Z. ACM SIGSOFT Softw. Eng. Notes Ian J. Hayes, Cliff B. Jones, John E. Nicholls
1993	—	`conf`	Deriving Modular Designs from Formal Specifications. SIGSOFT FSE David A. Carrington, David J. Duke, Ian J. Hayes, Jim Welsh
1992	J	`jnl`	A Case-Study in Timed Refinement: A Mine Pump. IEEE Trans. Software Eng. Brendan P. Mahony, Ian J. Hayes
1992	J	`jnl`	Multi-Relations in Z. Acta Informatica Ian J. Hayes
1992	—	`conf`	Towards Libraries for Z. Z User Workshop Ian J. Hayes, Luke Wildman
1992	J	`jnl`	VDM and Z: A Comparative Case Study. Formal Aspects Comput. Ian J. Hayes
1990	—	`conf`	Interpretations of Z Schema Operations. Z User Workshop Ian J. Hayes
1989	—	`conf`	A Generalisation of Bags in Z. Z User Workshop Ian J. Hayes
1989	—	`conf`	Signalling System No.7, The Network Layer. PSTV Ian J. Hayes, M. Mowbray, Gordon A. Rose
1987	J	`jnl`	Laws of Programming. Commun. ACM C. A. R. Hoare, Ian J. Hayes, Jifeng He, Carroll Morgan, A. W. Roscoe, Jeff W. Sanders, Ib Holm Sørensen, J. Michael Spivey, Bernard Sufrin
1986	J	`jnl`	Specification Directed Module Testing. IEEE Trans. Software Eng. Ian J. Hayes
1985	J	`jnl`	Applying Formal Specification to Software Development in Industry. IEEE Trans. Software Eng. Ian J. Hayes
1978	J	`jnl`	Some remarks on "Ambiguous Machine Architecture". SIGARCH Comput. Archit. News Ian J. Hayes