SPARK is a contractualized sublanguage of Ada which is unambiguous and suitable for rigorous static analysis. It has been extensively used in industrial applications where safety and security are paramount.

The tutorial will cover the rationale and design goals of SPARK, the core SPARK language, and SPARK analyses including information flow, exception freedom, and formal verification.

Practicing software engineers, programme managers, and those involved with procurement of high-integrity software systems might attend this tutorial. Some background in the development of safety- or securitycritical software might be useful, but not essential.

Presenter

Rod is a well-known conference speaker. He has presented papers, tutorials and workshops at many international events including STC, NSA HCSS, and ACM SIGAda. He was the opening keynote speaker at Ada Europe 2006.

Rod has been involved with the design of both safetyand security-critical software with Praxis for many years, including significant contributions to many of Praxis' keynote projects such as SHOLIS, MULTOS CA, Tokeneer, and the development of the SPARK language and verification tools.

Rod is a Chartered Engineer, a Fellow of the BCS, and an SEI-certified PSP Instructor.

>Back