SPARK Pro for Embedded and Systems Programming

Embedded systems are everywhere today, from the thermostats that manage a building’s temperature to the control systems in charge of jet engines. Clearly, much can depend on these operating correctly - imagine what might happen if a critical control system in your car failed as you’re driving.

SPARK Pro brings formal methods to industrial scale and delivers unbeatable security, correctness and proven memory safety for industrial-scale embedded and native applications. The SPARK language provides constructs specifically designed to facilitate interactions with hardware and to specify intended program behavior. And SPARK Pro provides formal assurance that the code behaves according to its specification. Finally, the GNAT compiler (using GCC or LLVM backends) generates efficient machine code for bare metal or OS-based systems. SPARK Pro delivers both high assurance and efficient execution of your code.

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

Join 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