Title :
Program development with SPARK
Author_Institution :
Program Validation Ltd., Southampton, UK
Abstract :
SPARK is an annotated subset of Ada for high-integrity programming. This subset, in conjunction with its system of annotations (formal comments), is designed to eliminate language ambiguities and insecurities, and to allow rigorous static code analysis and formal verification of programs. The development, flow analysis and correctness proof of SPARK programs is supported by a software tool, the SPARK Examiner. The paper outlines the essential features of SPARK and explains how the Examiner is used in program development
Keywords :
Ada; program verification; software reliability; software tools; Ada; SPARK; SPARK Examiner; correctness proof; flow analysis; formal verification; high-integrity programming; insecurities; language ambiguities; program development; software tool; static code analysis;
Conference_Titel :
High Integrity Ada, IEE Colloquium on
Conference_Location :
London
