Toward Ada Verification: A Collection of Relevant Topics
Abstract
IDA Paper P-1900, Towards Ada Verification: A Collection of Relevant Topics, is a survey of various topics in Ada verification, the state of progress in both near-term and far-term goals, and some possible directions for future work. Chapter 1 studies the extent to which the existing general purpose literature on program verification already covers the Ada language and concludes with an annotated bibliography. Chapter 2 surveys the possibility of adapting existing verification tools as near-term vehicles for Ada verification. Chapter 3 is a discussion of specification languages, cast in the form of a commentary on and criticism of ANNA, with suggestions for some extensions and improvements to it. Chapter 4 describes the far-term European project for a formal definition of the whole of Ada. It concludes with a brief discussion of the possibility of standards for the acceptance of verification systems. Chapter 5 presents the results of an attempt to survey as wide as possible a community of users, in particular, Ada users, on the ways in which, if at all, they use features of Ada which currently present problems for verification.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1986
- Accession Number
- ADA230611
Entities
People
- David Gauspari
- Doug Webber
- Jeffrey Hird
- John Mchugh
- Richard Platek
Organizations
- Institute for Defense Analyses