Content by Yannick Moy
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.
Proving Software Security with SPARK Pro
AdaCore Contribution to Reducing GHG Emissions
Like any other company, AdaCore contributes to climate change through its activities. We recognize that it is our responsibility to reduce this…
Memory Safety with Formal Proof
SPARK Pro for Embedded and Systems Programming
Explainable Program Proofs
Ever wanted to understand why program proof is not as easy as telling ChatGPT "can you prove that program <code>stuff</code> is correct for me?" A…
The Case for SPARK Evolution - an April First Parable
SPARK already allows you to specify functional contracts by cases, and soon it will allow you to specify cases that lead to an exception. But what…
When Formal Verification with SPARK is the Strongest Link
Security is only as strong as its strongest link. That's important to keep in mind for software security, with its long chain of links, from design…
I can’t believe that I can prove that it can sort
When an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this…
Proving the Correctness of GNAT Light Runtime Library
The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use…
SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)
SPARKNaCl is a SPARK version of the TweetNaCl cryptographic library, developed by formal methods and security expert Rod Chapman. For two years…
Enhancing the Security of a TCP Stack with SPARK
The developers of CycloneTCP library at Oryx Embedded partnered with AdaCore to replace the TCP part of the C codebase by SPARK code, and used the…
