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
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…
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy
AdaCore Tech Days Prez on SPARK
Yannick Moy
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…
Yannick Moy
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…
Yannick Moy
SPARK 2014 Rationale: Functional Update
While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently…
Yannick Moy
SPARK 2014 Rationale: Object Oriented Programming
Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known…
Tristan Gingold, Yannick Moy