A three-day course for software engineers, managers, and software assessment/regulation personnel, which presents the principles of high assurance software development and verification using SPARK.
The course explains the rationale of SPARK, describes the language and the principles of formal methods analysis, and shows how to use the SPARK language and the SPARK Pro Toolset both in new projects and in the context of existing (legacy) systems. This is done via instructor-led lecture, participatory quizzes, and hands-on lab exercises.
Software engineers, managers and regulators (assessors) involved with the development and verification of software.
The course can be conducted remotely or on site.
Previous experience with Ada is required.
If you have no previous experience with Ada: please refer to the Ada Essentials course in order to establish a foundation of knowledge in Ada prior to considering this training.
Formal Methods and SPARK
Proving the absence of runtime error
Advanced Flow Analysis
Please contact an AdaCore sales representative with any questions or requests for this training course via: email@example.com.