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
Prove in the Cloud
We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now…
Yannick Moy
SPARK Tutorial at FDL Conference
Researcher Martin Becker is giving a SPARK tutorial next week at FDL conference. This post gives a link to his tutorial material (cookbook and…
Yannick Moy
New SPARK Cheat Sheet
Our good friend Martin Becker has produced a new cheat sheet for SPARK, that you may find useful for a quick reminder on syntax that you have not…
Yannick Moy
Proving Loops Without Loop Invariants
For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to…
Yannick Moy
Research Corner - Focused Certification of SPARK in Coq
The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more…
Yannick Moy
Applied Formal Logic: Searching in Strings
A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of…
Yannick Moy
Research Corner - FLOSS Glider Software in SPARK
Two years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove…
Yannick Moy
Research Corner - Floating-Point Computations in SPARK
It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the…
Yannick Moy
Frama-C & SPARK Day Slides and Highlights
The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with…
Yannick Moy
New Guidance for Adoption of SPARK
While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on…
Yannick Moy
(Many) More Low Hanging Bugs
We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology.…
Yannick Moy, Emmanuel Briot, Nicolas Roche
A Usable Copy-Paste Detector in A Few Lines of Python
After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a…