Selected Publications

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.