Blog Posts 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.
Yannick Moy, Nicolas Venner, Paul Sivac, Tracey Gilbert
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…
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy, Lionel Matias
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…
Yannick Moy, Claire Dross
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…
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy
When the RISC-V ISA is the Weakest Link
Maxim Reznik, Yannick Moy
First Ada Virtual Conference organized by and for the Ada community
The Ada Community has gathered recently around a new exciting initiative - an Ada Virtual Conference, to present Ada-related topics in a 100% remote…
Yannick Moy, Raphaël Amiard, Tucker Taft
RFCs for Ada and SPARK evolution now on GitHub
Interested in participating in the evolution of the Ada or SPARK languages? We have something for you.
Yannick Moy, Nicolas Setton, Ben Brosgol