Mechanization of program construction in Martin-Loef's theory of types. - Andrew Ireland (1989)

Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs. - Alan Bundy; Frank van Harmelen; Alan Smaill; Andrew Ireland (CADE, 1990)

On the Use of the Constructive Omega-Rule within Automated Deduction. - Siani Baker; Andrew Ireland; Alan Smaill (LPAR, 1992)

The Use of Planning Critics in Mechanizing Inductive Proofs. - Andrew Ireland (LPAR, 1992)

Incresing the Versatility of Heuristic Based Theorem Provers. - Alistair Manning; Andrew Ireland; Alan Bundy (LPAR, 1993)

Rippling: A Heuristic for Guiding Inductive Proofs. - Alan Bundy; Andrew Stevens 001; Frank van Harmelen; Andrew Ireland; Alan Smaill (Artif. Intell., 1993)

On Exploiting the Structure of Martin-Löf's Theory of Types. - Andrew Ireland (Comput. J., 1993)

Proof Plans for the Correction of False Conjectures. - Raúl Monroy; Alan Bundy; Andrew Ireland (LPAR, 1994)

Extensions to a Generalization Critic for Inductive Proof. - Andrew Ireland; Alan Bundy (CADE, 1996)

Productive Use of Failure in Inductive Proof. - Andrew Ireland (J. Autom. Reason., 1996)

Invariant Discovery via Failed Proof Attempts. - Jamie Stark; Andrew Ireland (LOPSTR, 1998)

Towards Automatic Imperative Program Synthesis Through Proof Planning. - Jamie Stark; Andrew Ireland (ASE, 1999)

Interactive Proof Critics. - Andrew Ireland; Mike Jackson 003; Gordon Reid (Formal Aspects Comput., 1999)

Automatic Verification of Functions with Accumulating Parameters. - Andrew Ireland; Alan Bundy (J. Funct. Program., 1999)

Proof planning for strategy development. - Andrew Ireland; Jamie Stark (Ann. Math. Artif. Intell., 2000)

Higher Order Function Synthesis Through Proof Planning. - Andrew Cook; Andrew Ireland; Greg Michaelson (ASE, 2001)

Automation for Exception Freedom Proofs. - Bill J. Ellis; Andrew Ireland (ASE, 2003)

An Integration of Program Analysis and Automated Theorem Proving. - Bill J. Ellis; Andrew Ireland (IFM, 2004)

Invariant Patterns for Program Reasoning. - Andrew Ireland; Bill J. Ellis; Tommy Ingulfsen (MICAI, 2004)

Rippling - meta-level guidance for mathematical reasoning. - Alan Bundy; David A. Basin; Dieter Hutter; Andrew Ireland (Cambridge University Press, 2005)

Tool Integration for Reasoned Programming. - Andrew Ireland (VSTTE, 2005)

Discovering applications of higher order functions through proof planning. - Andrew Cook; Andrew Ireland; Greg Michaelson; Norman Scaife (Formal Aspects Comput., 2005)

Low-Level Programming in Hume: An Exploration of the HW-Hume Level. - Kevin Hammond; Gudmund Grov; Greg Michaelson; Andrew Ireland (IFL, 2006)

Towards Automatic Assertion Refinement for Separation Logic. - Andrew Ireland (ASE, 2006)

Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis. - Andrew Ireland; Jamie Stark (Autom. Softw. Eng., 2006)

An Integrated Approach to High Integrity Software Verification. - Andrew Ireland; Bill J. Ellis; Andrew Cook; Roderick Chapman; Janet Barnes (J. Autom. Reason., 2006)

Formal verification of concurrent scheduling strategies using TLA. - Gudmund Grov; Greg Michaelson; Andrew Ireland (ICPADS, 2007)

PARTES: Performance Analysis of Real-Time Embedded Systems. - Benjamin Gorry; Andrew Ireland; Peter King (QEST, 2007)

Preserving coordination properties when transforming concurrent system components. - Gudmund Grov; Robert F. Pointon; Greg Michaelson; Andrew Ireland (SAC, 2008)

Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. - Andrew Ireland; Gudmund Grov; Michael J. Butler (ASM, 2010)

Towards Automated Property Discovery within Hume. - Gudmund Grov; Andrew Ireland (WING@ETAPS/IJCAR, 2010)

Refinement and Term Synthesis in Loop Invariant Generation. - Ewen Maclean; Andrew Ireland; Lucas Dixon; Robert Atkey (WING@ETAPS/IJCAR, 2010)

Synthesising Functional Invariants in Separation Logic. - Ewen Maclean; Andrew Ireland; Gudmund Grov (WING@ETAPS/IJCAR, 2010)

Guest Editorial. - Andrew Ireland; Willem Visser (Autom. Softw. Eng., 2010)

Introduction. - Martin Giese; Andrew Ireland; Laura Kovács (J. Symb. Comput., 2010)

Mutation in Linked Data Structures. - Ewen Maclean; Andrew Ireland (ICFEM, 2011)

The CORE system: Animation and functional correctness of pointer programs. - Ewen Maclean; Andrew Ireland; Gudmund Grov (ASE, 2011)

Refinement Plans for Informed Formal Design. - Gudmund Grov; Andrew Ireland; Maria Teresa Llano (ABZ, 2012)

E-SPARK: Automated Generation of Provably Correct Code from Formally Verified Designs. - Rajiv Murali; Andrew Ireland (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

Reasoned modelling critics: Turning failed proofs into modelling guidance. - Andrew Ireland; Gudmund Grov; Maria Teresa Llano; Michael J. Butler (Sci. Comput. Program., 2013)

A Verification Condition Visualizer. - Madiha Jami; Andrew Ireland (VSTTE, 2014)

Discovery of invariants through automated theory formation. - Maria Teresa Llano; Andrew Ireland; Alison Pease (Formal Aspects Comput., 2014)

A Rigorous Approach to Combining Use Case Modelling and Accident Scenarios. - Rajiv Murali; Andrew Ireland; Gudmund Grov (NFM, 2015)

Preface. - Gudmund Grov; Andrew Ireland (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

Semi-Automated Design Space Exploration for Formal Modelling. - Gudmund Grov; Andrew Ireland; Maria Teresa Llano; Peter Kovacs; Simon Colton; Jeremy Gow (ABZ, 2016)

UC-B: Use Case Modelling with Event-B. - Rajiv Murali; Andrew Ireland; Gudmund Grov (ABZ, 2016)

Proof automation for functional correctness in separation logic. - Ewen Maclean; Andrew Ireland; Gudmund Grov (J. Log. Comput., 2016)

Preface of the special issue for AVoCS 2015. - Gudmund Grov; Andrew Ireland (Sci. Comput. Program., 2017)

The Use of Automated Theory Formation in Support of Hazard Analysis. - Andrew Ireland; Maria Teresa Llano; Simon Colton (NFM, 2018)

An Argumentation and Ontology Based Legal Support System for AI Vehicle Design. - Yiwei Lu; Zhe Yu; Yuhui Lin; Burkhard Schafer 001; Andrew Ireland; Lachlan Urquhart (JURIX, 2022)

Logic and Theory Repair in Legal Modification. - Yiwei Lu; Yuhui Lin; Xue Li 018; Alan Bundy; Burkhard Schäfer 001; Andrew Ireland (COGAI@IJCLR, 2023)

A Legal System to Modify Autonomous Vehicle Designs in Transnational Contexts. - Yiwei Lu; Zhe Yu; Yuhui Lin; Burkhard Schafer 001; Andrew Ireland; Lachlan Urquhart (JURIX, 2023)

Anticipating Accidents through Reasoned Simulation. - Craig Innes; Andrew Ireland; Yuhui Lin; Subramanian Ramamoorthy (TAS, 2023)