NuSPADE: An Integrated Approach to Program Reasoning
[
pdf ,
ps ]
NuSPADE: An Integrated Approach to Exception Freedom Proof
Presented at the SPARK User Meeting,
Praxis High Integrity Systems Ltd. Bath, 2004
[
pdf ]
Extended version [
ps ]
Invariant Patterns for Program Reasoning
Presented at the 3rd Mexican International Conference on Artificial Intelligence,
Mexico City, 2004
[ ppt ]
An Integration of Program Analysis and Automated Theorem Proving
Presented at the 4th International Conference on Integrated Formal Methods,
Canterbury, 2004
[ ppt ]
The Verifying Compiler
Presented at Grand Challenges of Computing Conference: Dependable Evolving
Systems (Proposal 6),
Newcastle, 2004
[ ppt ]
Proving Exception Freedom within High Integrity Software Systems
Presented at CIAO-03,
Dagstuhl, Germany, 2003
[ ppt ]
Increasing Automation for Exception Freedom Proofs
Presented at the FORTEST Network workshop series,
Bath, 2003
[ ppt ]
NuSPADE: Automation for Exception Freedom Proofs
Presented at the 18th IEEE International Conference on Automated Software Engineering
(ASE),
Montreal, 2003
[ ppt ]
The Use of Patterns to Guide Code Certification: A Proposal
Presented at the NASA Ames Workshop on Frontiers of Automated Software Engineering,
Mountain View CA, 2003
[ ppt ]
Proving Exception Freedom within High Integrity Software Systems
Presented at the Scottish Theorem Proving seminar series,
Heriot-Watt, Edinburgh, 2003
[ ppt ]
Proof Automation for the SPARK Approach to High Integrity Ada
Presented at the FORTEST Network workshop series,
University of York, 2002
[ ppt ]
Proof Automation for the SPARK Approach to High Integrity Ada
Presented at the Technical Cooperation Panel (TTCP) Workshop:
NATO Defence related system and software safety issues,
University of York, 2002
[ ppt ]
Proof Automation for the SPARK Approach to High Integrity Ada
Presented at CIAO-02,
Edinburgh, 2002
[ ppt ]
Proof Automation for the SPARK Approach to High Integrity Ada
Presented at the second workshop on Automated Verification of Critical Systems (AVoCS-02)
University of Birmingham, 2002
[ ppt ]
Automatic Guidance for the Formal Verification of High Integrity Ada
Presented at the first workshop on Automated Verification of Critical Systems (AVoCS-01)
University of Oxford, 2001
[ ps ]
Towards Proof Planning for High Integrity Software
Presented at the 8th Workshop on Automated Reasoning,
York, 2001
[ ps ]