SPARK Essentials

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.

Target Audience

Software engineers, managers and regulators (assessors) involved with the development and verification of software.

Course Duration

3 days

Location

The course can be conducted remotely or on site.

Prerequisites

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.

Course Contents

Introduction

• Formal Methods and SPARK

• SPARK Language

• SPARK Tools
  
  

Proving Code

• Flow Analysis

• Proving the absence of runtime error

• Specification Language

• Subprogram Contracts

• Type Contracts
  
  

Advanced SPARK

• Advanced Proof

• Advanced Flow Analysis

• Pointer Programs

• Auto-active Proof

• State Abstraction

• SPARK Boundary

Please contact an AdaCore sales representative with any questions or requests for this training course via: sales@adacore.com.