**A. Ireland and G. Grov and M. Butler**
Reasoned modelling critics: turning failed proofs into modelling guidance,
In *Proceedings of ABZ 2010*, LNCS, Springer, 2010 [ to appear ]

**A. Ireland and G. Grov**
Reasoned Modelling: Combining Proof and Modelling Patterns to Guide Systems
Design.
In *Refinement Based Methods for the Construction of Dependable Systems:
09381 Extended Abstracts Collection*.
Editors J-R. Abrial, M. Butler, R. Joshi, E. Troubitsyna, J.C.P. Woodcock.
Dagstuhl Seminar Proceedings, Schloss Dagstuhl - Leibniz-Zentrum fuer
Informatik, 2010. [ link ]

**A. Pease, A. Smaill, S. Colton, A. Ireland, M.T. Llano, R. Ramezani, G. Grov,
M. Guhe**
Applying Lakatos-style Reasoning to AI Problems.
In *Thinking Machines and the philosophy of computer science: Concepts and
principles*,
J. Vallverdu (Ed), IGI Global, PA, USA, 2010 (To Appear).

**G. Grov and A. Ireland**
Towards Automated Property Discovery within Hume.
In *2nd International Workshop on Invariant Generation (WING'09)*,
a satellite workshop of ETAPS-09, York, UK, 2009.

**E. Maclean, A. Ireland, R. Atkey, L. Dixon**
Refinement and Term Synthesis in Loop Invariant Generation.
In *2nd International Workshop on Invariant Generation (WING'09)*,
a satellite workshop of ETAPS-09, York, UK, 2009.

**B. Gorry, A. Ireland, and P. King.**
Sensitivity analysis of real-time.
In *Proceedings of WASET*, pages 12--19, 2008.

**G. Grov, R. Pointon, G. Michaelson, and A. Ireland**
Preserving Coordination Properties when Transforming Concurrent System Components.
In *Coordination Models, Languages and Applications Track of the
23rd Annual ACM Symposium on Applied Computing*, volume 1 of 3 of ACM,
pages 126 -- 127, The Association for Computing Machinery, Inc. 2008.

**G. Grov, G. Michaelson, and A. Ireland**
Formal Verification of Concurrent Scheduling Strategies using TLA.
In *3rd IEEE International Workshop on Scheduling and Resource
Management for Parallel and Distributed Systems*. ACM Press, 2007.

**A. Ireland**
Tool integration for reasoned programming.
In *Proceedings of IFIP TC2 (Programming) WG2.3 (Programming
Methodology) Working Conference "Verified Software: Tools, Techniques, and
Experiments" (VSTTE, Zurich, Oct. 10-13, 2005)*, volume 4171 of LNCS.
Springer-Verlag, 2008.

**A. Ireland**
Cooperative reasoning for automatic software verification.
In *Proceedings of the second workshop on Automated Formal
Methods (AFM`07)*, pages 51--54. ACM, 2007.
A satellite workshop of the 22nd IEEE/ACM International Conference
on Automated Software Engineering (ASE`07).

**A. Ireland**
A cooperative approach to loop invariant discovery for pointer programs.
In *Proceedings of 1st International Workshop on Invariant
Generation (WING)*, a satellite workshop of Calculemus 2007,
held at RISC, Hagenberg, Austria, 2007.
Appears within the RISC Report Series
RISC Report Series University of Linz, Austria.

**A. Ireland, B.J. Ellis, A. Cook, R. Chapman and J.Barnes**
An Integrated Approach to High Integrity Software Verification,
*Journal of Automated Reasoning: Special Issue on Empirically
Successful Automated Reasoning*, Kluwer, vol 36(4), 379-410, 2006.

**A. Ireland**
Towards Automatic Assertion Refinement for Separation Logic,
*Proceedings of the 21st IEEE International Conference on Automated
Software Engineering*, IEEE Computer Society, 2006.
A longer version is available
from the School of Mathematical and Computer Sciences,
Heriot-Watt University, as Technical Report HW-MACS-TR-0039.

**A. Bundy, D. Basin, D. Hutter, A. Ireland.**
Rippling: Meta-level Guidance for Mathematical Reasoning
*Cambridge University Press*, April 2005.
(see also
rippling homepage).

**A. Cook, A. Ireland, G.J. Michaelson, N. Scaife.**
Discovering Applications of Higher Order Functions Through Proof Planning,
*Journal of Formal Aspects of Computing*,
Accepted for publication 2004.

**A. Ireland, B.J. Ellis, A. Cook, R. Chapman, J. Barnes.**
An Integrated Approach to Program Reasoning,
*Submitted to the Journal of Formal Aspects of Computing:
Special Issue on Integrated Formal Methods*, 2004.
Available from School of Mathematical and Computer Sciences,
Heriot-Watt University, Technical Report HW-MACS-TR-0027.
[ pdf ]

**A. Ireland and J. Stark.**
Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis,
*Journal of Automated Software Engineering*,
Springer-Verlag, Accepted for publication, 2004.
Also available from School of Mathematical and Computer Sciences,
Heriot-Watt University, Technical Report HW-MACS-TR-0026.
[ pdf ]

**B.J. Ellis and A. Ireland.**
An Integration of Program Analysis and Automated Theorem Proving,
In *Proceedings of the
4th International Conference on Integrated Formal Methods (IFM-04)*,
Editors: Boiten, E.A. and Derrick, J. and Smith, G.
Lecture Notes in Computer Science No. 2999, Springer Verlag, 2004.
Available from School of Mathematical and Computer Sciences,
Heriot-Watt University, Technical Report HW-MACS-TR-0014
[ pdf ]

**A. Ireland, B.J. Ellis, T. Ingulfsen.**
Invariant Patterns for Program Reasoning
In *Proceedings of the
3rd Mexican International Conference on Artificial Intelligence (MICAI-04)*,
Editors: Monroy, R. and Arroyo-Figueroa, G. and Sucar, L.E. and Sossa, H.
Lecture Notes in Artificial Intelligence No. 2972, Springer Verlag, 2004.
Available from School of Mathematical and Computer Sciences, Heriot-Watt University,
Technical Report HW-MACS-TR-0011.
[ pdf ]

**A. Ireland.**
A Practical Perspective on the Verifying Compiler Proposal,
In *Proceedings of the
Grand Challenges in Computing Research Conference*,
BCS, IEE and UKCRC, 2004.
Available from School of Mathematical and
Computer Sciences, Heriot-Watt University,
Technical Report HW-MACS-TR-0025.
[ pdf ]

**A. Ireland.**
Towards Increased Verification Automation for High Integrity Software Engineering,
*European Research Consortium for Informatics and
Mathematics News: Special Issue on Automated Software Engineering*,
No. 58, 2004.
[ doc,
html
]

**B.J. Ellis and A. Ireland.**
Automation for Exception Freedom Proofs,
In *Proceedings of the
18th IEEE International Conference on Automated Software Engineering*,
IEEE Computer Society, 2003.
Available from School of Mathematical and Computer Sciences,
Heriot-Watt University, Technical Report HW-MACS-TR-0010.
[ pdf ]

** A. Ireland and J. Stark.**
Proof Planning for Strategy Development,
*Annals of Mathematics and Artificial Intelligence*,
Editor: H. Kirchner,
Vol. 29:1-4, Kluwer Academic Publishers,
2001.

**A. Cook, A. Ireland, G.J. Michaelson.**
Higher Order Function Synthesis through Proof Planning.
In *Proceedings of the 16th IEEE International Conference on Automated Software Engineering.*
IEEE Computer Society, 2001.

**A. Ireland.**
Proof Planning for Hardware Verification.
In *Proceedings of the Internationl Workshop on Advances in Verification (WAVe 2000)*,
affiliated with the Conference on Computer-Aided Verification (CAV 2000), Chicago, USA, 2000.

**A. Ireland, M. Jackson, G. Reid.**
Interactive Proof Critics.
*Journal of Formal Aspects of Computing: Special Issue on User Interfaces for Theorem Provers*,
11(3):302-325, 1999.
Available from Dept. of
Computing and Electrical Engineering, Heriot-Watt University, Research Memo
RM/98/15.

**J. Stark and A. Ireland.**
Towards Automatic Imperative Program Synthesis through Proof Planning,
In *Proceedings of the 14th IEEE International Conference on
Automated Software Engineering*,
IEEE Computer Society, 1999.

**J. Stark and A. Ireland.**
Invariant Discovery via Failed Proof Attempts.
In P. Flener, editor, * Logic-Based Program Synthesis and
Transformation*, LNCS No. 1559, pages 271-288. Springer-Verlag, 1998.
An earlier version is available from the Dept. of Computing and
Electrical Engineering, Heriot-Watt University, Research Memo RM/98/2.

**M. Fisher and A. Ireland.**
Towards a Science of Reasoning through Societies of Proof Planning Agents.
In *Proceedings of the International Workshop on Using AI Methods in Deduction*
affiliated with the 15th Conference on Automated Deduction (CADE-15),/em>,
Lindau Germany, 1998.

**A. Ireland and J. Stark.**
On the Automatic Discovery of Loop Invariants.
In *Proceedings of the Fourth NASA Langley Formal Methods Workshop*,
NASA Conference Publication 3356, 1997.
Also available from Dept. of Computing and Electrical Engineering,
Heriot-Watt University, Research Memo RM/97/1.

**A. Ireland and A. Bundy.**
Automatic Verification of Functions with Accumulating Parameters.
*Journal of Functional Programming: Special Issue on Theorem
Proving and Functional Programming,*, 9(2):225--245, 1999.
A longer version is available from Dept. of Computing and Electrical
Engineering, Heriot-Watt University, Research Memo RM/97/11.

**G.J. Michaelson, A. Ireland, P.J.B. King.**
Towards a skeleton based parallelising compiler for standard ML.
In *Proceedings of the 9th International Workshop on Implementation of
Functional Languages (IFL'97)*, pages 539-546, St Andrews, 1997.

**A. Ireland and A. Bundy.**
Extensions to a Generalization Critic for Inductive Proof.
*13th Conference on Automated Deduction (CADE-13)*, pages 47-61.
Springer Lecture Notes in Artificial Intelligence No. 1104.
Springer-Verlag, 1996.

**A. Ireland and A. Bundy.**
Productive Use of Failure in Inductive Proof.
*Journal of Automated Reasoning*, 16(1-2):79-111, 1996.

**R. Monroy, A. Bundy, A. Ireland.**
Proof Plans for the Correction of False Conjectures.
In F. Pfenning, editor,
*Proceedings of the 5th International Conference on
Logic Programming and Automated Reasoning (LPAR'94)*,
Kiev, Ukraine,
Lecture Notes in Artificial Intelligence, Vol 822, pages 54-68,
1994. Springer-Verlag.

**A. Ireland.**
On Exploiting the Structure of Martin-Lof's Theory of Types.
*The Computer Journal*, 36(4):387--398, 1993.

**A. Manning, A. Ireland, A. Bundy.**
Increasing the Versatility of Heuristic Based Theorem Provers.
In A. Voronkov, editor,
*Proceedings of the International Conference on Logic
Programming and Automated Reasoning (LPAR'93)*,
St. Petersburg,
Lecture Notes in Artificial Intelligence Vol 698, pages pp 194-204.
Springer-Verlag, 1993.

**A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, A. Smaill.**
Rippling: A Heuristic for Guiding Inductive Proofs.
*Journal of Artificial Intelligence,*, 62:185--253, 1993.

**A. Ireland.**
The Use of Planning Critics in Mechanizing Inductive Proofs.
In A. Voronkov, editor,
*Proceedings of the International Conference on Logic Programming and Automated
Reasoning (LPAR'92), St. Petersburg*, pages 178-189,
Lecture Notes in Artificial Intelligence No. 624,
Springer-Verlag, 1992.

**S. Baker, A. Ireland, A. Smaill.**
On the Use of the Constructive Omega Rule within Automated Deduction.
In A. Voronkov, editor,
*Proceedings of the International Conference on Logic
Programming and Automated Reasoning (LPAR'92)*, St. Petersburg,
Lecture Notes in Artificial Intelligence No. 624, pages 214-225.
Springer-Verlag, 1992.

**A. Ireland.**
On Exploiting the Structure of Martin-Lof's Theory of Types.
In Hermann Kaindl, editor,
*Proceedings of the Seventh Austrian Conference on Artificial Intelligence
(Tagung'91)*, Vienna, Springer-Verlag, Informatik-Fachberichte 287, 1991.

**A. Bundy, F. van Harmelen, A. Smaill, and A. Ireland.**
Extensions to the Rippling-out Tactic for Guiding Inductive Proofs.
In M.E. Stickel, editor,
*Proceedings of the 10th International Conference on Automated Deduction (CADE-10)*,
Lecture Notes in Artificial Intelligence No. 449, pages 132-146,
Springer-Verlag, 1990.