NuSPADE: Publications and Research Papers

Ireland, A. and Ellis, B.J. and Cook, A. and Chapman, R. and Barnes, J. An Integrated Approach to High Integrity Software Verification, A shorter version of this paper has been accepted for publication in the Journal of Automated Reasoning: Special Issue on Empirically Successful Automated Reasoning, 2004. Available from School of Mathematical and Computer Sciences, Heriot-Watt University, Technical Report HW-MACS-TR-0027. [ pdf ]

Ireland, A. and Stark, J. 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 ]

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

Ellis, B.J. and Ireland, A. Automation for Exception Freedom Proofs, 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 ]

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

Ireland, A. A Practical Perspective on the Verifying Compiler Proposal, 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 ]

Ireland, A. 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 ]

Ingulfsen, T. Automatic Generation of Algorithmic Properties (AutoGAP), Undergraduate BSc Computer Science Project Dissertation, School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, 2003. [ pdf ]

Related Publications

Ireland, A. The Use of Planning Critics in Mechanizing Inductive Proofs. 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.

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

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

Ireland, A. and Bundy, A. Automatic Verification of Functions with Accumulating Parameters. To appear in the Journal of Functional Programming: Special Issue on Theorem Proving & Functional Programming, 1997. A longer version is available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/97/11.

Ireland, A. Jackson, M. and Reid, G. Interactive Proof Critics. Submitted to a Special Issue of the Journal of Formal Aspects of Computing on User Interfaces for Theorem Provers. Available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/98/15.

Ireland, A. and Stark, J. On the Automatic Discovery of Loop Invariants. 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.

Stark, J. and Ireland, A. 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.

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

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