The SpAda? project is an effort by the SAnToS Lab to develop an integrated development environment for SPARK/Ada -- a subset of Ada for high assurance applications developed by Praxis High Integrity Systems . This IDE will leverage the Eclipse IDE and provide some sophisticated analysis that uses the Sireum engine. In other words, SpAda? is a collection of plugins to Eclipse that uses the Sireum libraries to perform the analysis.

SpAda? provides integrated support for the Praxis SPARK Examiner -- a static checking tool that enforces very coding rules and information flow requirements. SpAda? is integrated with AdaCore?'s GNATBench Eclipse plug-in for Ada. Future versions of SpAda? will provide advanced analysis capabilities to aid developers in constructing information flow specifications based on SPARK's "derives" annotations. Our ultimate vision involves extending SpAda? so that it becomes an integrated development environment that specifically targets development of information assurance applications in SPARK.