Memory Safety with Formal Proof

Discover how to prove that code cannot fail at runtime, including proof of memory safety and correct data initialization, by using SPARK Pro. You’ll learn more about proven memory safety for industrial-scale embedded and native applications, as well as how to ensure memory safety either at runtime or by static analysis.

Join this session to learn more about:

• How to detect and prevent runtime errors
• How memory safety can be ensured either at runtime or by static analysis
• How to enforce correct data initialization
• Use of preconditions and postconditions to prove absence of runtime errors
• Use of proof levels to prove absence of runtime errors

Memory management is a delicate issue in critical embedded software. Memory is a limited resource, and many typical software errors that jeopardize the integrity of software execution are due to unsafe memory management.

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

Missed our previous webinar in this series? Watch SPARK Pro for Embedded and Systems Programming here: https://www.youtube.com/watch?v=97G1V2U8Drk