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
Authors
M. Anthony Aiello
Tony Aiello is a Product Manager at AdaCore. Currently, he manages SPARK Pro, GNAT Pro for Rust, and GNAT IQ.
Yannick Moy
Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.
