Software Engineering with SPARK 2014

Course#: BSEMB1001

About this Course

Course Type Course Code Duration
Embedded Software BSEMB1001 5 Days

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.

Why Attend this Course?

What Makes this Course Stand Apart?

What you will Learn?


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 Outline

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

What next- How do I arrange a group course or book a public place.?

We are here to help so please utilise our live chat team

Call to speak to your account manager or a consultant on

+44 (0)345 467 9557 or email

We are all technical with a wealth of Learning & Development experience
so can talk you through any specific requirements or the details of
one of our courses.


Start typing and press Enter to search