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
The Most Obscure Arithmetic Run-Time Error Contest
Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course,…
Yannick Moy
Research Corner - SPARK 2014 vs Frama-C vs Why3
Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote…
Yannick Moy
Research Corner - Proving Security of Binary Programs with SPARK
Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on…
Yannick Moy
GNATprove Tips and Tricks: Using the Lemma Library
A well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of…
Yannick Moy
Did SPARK 2014 Rethink Formal Methods?
David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington…
Yannick Moy
Formal Verification of Legacy Code
Yannick Moy
SPARK Prez at New Conference on Railway Systems
RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write…
Yannick Moy, Emma Adby
Ada Lovelace Bicentennial
Yannick Moy
GNATprove Tips and Tricks: What’s Provable for Real?
SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known…
Yannick Moy
SPARK 2014 Rationale: Support for Ravenscar
As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in…
Yannick Moy
GNATprove Tips and Tricks: User Profiles
One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until…
Yannick Moy
The Eight Reasons For Using SPARK
Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most…