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.

• Purchase a copy of the book High Integrity Software The SPARK Approach to Safety and Security from Pearson.
• Introducing SPARK Pro (Webinar)
• SPARK Pro Website
• SPARK Training
• SPARK Engineering Services
• Supported Evaluation