Software Engineering with SPARK 2014

5 Day Course

A five-day course for programmers, managers, and software assessment/regulation personnel, which presents the principles of high assurance software development and verification using SPARK 2014. The course explains the rationale of SPARK 2014, describes the language and the principles of static code 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.

Target Audience Aimed at engineers, managers and regulators (assessors) involved with the development and verification of high assurance software. No previous experience with SPARK or Ada is required

Course Duration 5 days

Contents

• The SPARK/Ada programming language - types, expressions, statements, subprograms, packages.
• Introduction to static analysis and formal verification
• Data dependency analysis
• Flow dependency analysis
• Programming with contracts
• Modular / hybrid verification
• Proving absence of run-time exceptions
• Designing a SPARK program
• State abstraction