| 2023 | JURIX | A Legal System to Modify Autonomous Vehicle Designs in Transnational Contexts. | Yiwei Lu, Zhe Yu, Yuhui Lin, Burkhard Schafer, Andrew Ireland, Lachlan Urquhart |
| 2022 | JURIX | An Argumentation and Ontology Based Legal Support System for AI Vehicle Design. | Yiwei Lu, Zhe Yu, Yuhui Lin, Burkhard Schafer, Andrew Ireland, Lachlan Urquhart |
| 2011 | ICFEM | Mutation in Linked Data Structures. | Ewen Maclean, Andrew Ireland |
| 2010 | CADE | Towards Automated Property Discovery within Hume. | Gudmund Grov, Andrew Ireland |
| 2010 | CADE | Refinement and Term Synthesis in Loop Invariant Generation. | Ewen Maclean, Andrew Ireland, Lucas Dixon, Robert Atkey |
| 2010 | CADE | Synthesising Functional Invariants in Separation Logic. | Ewen Maclean, Andrew Ireland, Gudmund Grov |
| 2008 | SAC | Preserving coordination properties when transforming concurrent system components. | Gudmund Grov, Robert F. Pointon, Greg Michaelson, Andrew Ireland |
| 2007 | ICPADS | Formal verification of concurrent scheduling strategies using TLA. | Gudmund Grov, Greg Michaelson, Andrew Ireland |
| 2004 | IFM | An Integration of Program Analysis and Automated Theorem Proving. | Bill J. Ellis, Andrew Ireland |
| 1998 | LOPSTR | Invariant Discovery via Failed Proof Attempts. | Jamie Stark, Andrew Ireland |
| 1996 | CADE | Extensions to a Generalization Critic for Inductive Proof. | Andrew Ireland, Alan Bundy |
| 1994 | LPAR | Proof Plans for the Correction of False Conjectures. | Ral Monroy, Alan Bundy, Andrew Ireland |
| 1993 | LPAR | Incresing the Versatility of Heuristic Based Theorem Provers. | Alistair Manning, Andrew Ireland, Alan Bundy |
| 1992 | LPAR | On the Use of the Constructive Omega-Rule within Automated Deduction. | Siani Baker, Andrew Ireland, Alan Smaill |
| 1992 | LPAR | The Use of Planning Critics in Mechanizing Inductive Proofs. | Andrew Ireland |
| 1990 | CADE | Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs. | Alan Bundy, Frank van Harmelen, Alan Smaill, Andrew Ireland |