|
(via comp.lang.ada)
Recently, there has been significant interest in the use of Abstract Interpretation (AI) technology in the static analysis of critical software. A number of AI-based tools exist, but some of their marketing suffers from a level of hyperbole that is at best optimistic, and at worst somewhat irresponsible.
There have also been some attempts to compare AI-based static analysis tools with the analysis implemented by the SPARK language and the SPARK Examiner toolset. The aim of this white paper is to dispel some of the common myths and to avoid potential confusion with customers.
SPARK is based on carefuly designed Ada subset, which when coupled with annotatations can be analyzed and reasoned about using the SPARK Examiner. In most respects it follows the now classic model of progammer supplied assertions. The maturitiy and capabilties of the tool set are quite impressive.
Posted to Software-Eng by Ehud Lamm on 9/23/01; 11:04:20 AM
|
SPARK and Abstract Interpretation
