SPARK Pro for Embedded and Systems Programming

SPARK Pro brings formal methods to industrial scale and delivers unbeatable security, correctness and proven memory safety for industrial-scale embedded and native applications.

In this webinar, Yannick Moy outlines key features of SPARK Pro, including demos on pointer ownership, function contracts and safe type casting.

Watch this session to learn more about:

- The rich possibilities for data representation in SPARK

- Available contracts on data types

- The ownership principle for tracking pointers to data

- Available contracts on functions

- Handling of bindings with C libraries, safe type casting, software-hardware interactions

- Specializing the analysis for a given target platform