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.