About this event
In software security, subtle bugs arise from corner cases when the software doesn’t quite match its intent. While testing may enable programmers to find these bugs, formal methods go further and help programmers to prove their absence.
In this webinar, Yannick Moy outlines key features of SPARK Pro for proving that code obeys its specification, including the language to express this specification, and the process to successfully prove compliance.
SPARK Pro brings formal methods to industrial scale and delivers unbeatable security, correctness and proven memory safety for industrial-scale embedded and native applications.
Join this session to learn more about:
- The powerful specification language in SPARK
- Expressing natural language specifications as contracts in the code
- How special “ghost” code can help with specification
- How to use ghost code to develop proofs as code
- How SPARK Pro supports the user with detailed feedback
Can't make that time? Sign up to receive a recording of the webinar after the session.
Hosted by
-
Team member
Yannick MoyT
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. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com).
AdaCore
Helping People Build Software that MattersAdaCore provides commercial software solutions for Ada, SPARK, Rust, C and C++, helping developers build safe and secure software that matters.
