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.

Key takeaways from this webinar include:

- 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