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
VerifyThis Challenge in SPARK
This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program…
Yannick Moy
GNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)
Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first…
Yannick Moy
Two Projects to Compute Stats on Analysis Results
Two projects by Daniel King and Martin Becker facilitate the analysis of GNATprove results by exporting the results (either from the log or from the…
Fabien Chouteau, Arnaud Charlet, Yannick Moy
SPARK Tetris on the Arduboy
Yannick Moy
Rod Chapman on Software Security
Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how…
Yannick Moy
Proving Tetris With SPARK in 15 Minutes
I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the…
Raphaël Amiard, Yannick Moy, Pierre-Marie de Rodat
Going After the Low Hanging Bug
At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our…
Yannick Moy
New Year's Resolution for 2017: Use SPARK, Say Goodbye to Bugs
NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities" in which they single out five approaches which have…
Yannick Moy
SPARK Cheat Sheets (en & jp)
The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My…
Yannick Moy
GNATprove Tips and Tricks: What’s Provable for Real Now?
One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK).…
Yannick Moy
Research Corner - SPARK on Lunar IceCube Micro Satellite
Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar…
Yannick Moy
Verified, Trustworthy Code with SPARK and Frama-C
Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified,…