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
Authors
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.
M. Anthony Aiello
Tony Aiello is a Product Manager at AdaCore. Currently, he manages SPARK Pro and GNAT IQ.
