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.
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…
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…
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…
New Book About SPARK 2014
I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by…
SPARK 2014 Rationale: Type Predicates
Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar…
SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification
In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free…
How Our Compiler Learnt From Our Analyzers
Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent…
A Building Code for Building Code
In a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software…
GNATprove Tips and Tricks: Minimizing Rework
As automatic proof is time consuming, it is important that rework following a change in source code is minimized. GNATprove uses a combination of…
AdaCore Tech Days Prez on SPARK
GNATprove Tips and Tricks: Catching Mistakes in Contracts
Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by…
GNATprove Tips and Tricks: Keeping Justifications Up-To-Date
GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications…