Tokeneer Discovery - A SPARK Tutorial

Summary

This tutorial demonstrates the key capabilities of the SPARK and how it can verify SPARK programs are free from certain classes of bugs. A number of these are listed in the top twenty five most dangerous programming errors, including buffer overflow, input validation and uninitialized variables. SPARK is more suitable than other standard imperative programming languages such as C and C++ in engineering software for sectors that rely on the integrity of their software systems.

Finding More Information

Further information on SPARK and SPARK Pro can be obtained from the following sources.