Roderick Chapman & Neil White - Developing safe and secure code with SPARK

Roderick Chapman and Neil White present SPARK, a programming language and verification toolset designed for high-integrity systems like aerospace.

SPARK is a programming language for systems that protect life, security, or your reputation. It's rather unusual, because it emphasizes verification above other design goals. Over more than two decades, it has seen substantial success in some sectors, such as aerospace (the Typhoon aircraft, for example), rail signalling, jet engines, and air-traffic control. If you've flown in or out of the UK in the past 6 years, then your life has depended on SPARK. In additional to notable commercial success, the entire language and toolset are maintained as "FLOSS", and are available under the GPL for makers, the free software community and students. It offers a verification system based on static analysis and theorem proving that prevents many defects, such as buffer overflow, entirely and efficiently. It also supports Contracts in the language (like pre-conditions and assertions) that can be verified by the theorem prover, going far beyond just the usual "dumb bugs" and onto verification of application-specific properties. This talk presents a deep dive into SPARK - why it exists in the first place, how it works, and some example applications. If you think Rust is the state of the art in systems programming languages, then this talk is probably for you... PS... Our SPARK has nothing to do with Apache SPARK. If you're into Big Data and Hadoop, then this talk won't be what you expect...but come along anyway - you might learn something new.