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, Nicolas Roche, Pierre-Marie de Rodat, Fabien Chouteau
AdaCore at FOSDEM 2019
Like last year, we've sent a squad of AdaCore engineers to participate in the celebration of Open Source software at FOSDEM. Like last year, we had…
Yannick Moy
Amazon Relies on Formal Methods for the Security of AWS
Byron Cook, who founded and leads the Automated Reasoning Group at Amazon Web Services (AWS) Security, gave a powerful talk at the Federated Logic…
Fabien Chouteau, Emma Adby, Yannick Moy
Learn.adacore.com is here
We are very proud to announce the availability of our new Ada and SPARK learning platform learn.adacore.com, which will replace AdaCoreU(niversity)…
Yannick Moy
Security Agency Uses SPARK for Secure USB Key
ANSSI, the French national security agency, has published the results of their work since 2014 on designing and implementing an open-hardware &…
Yannick Moy, Roderick Chapman
How Ada and SPARK Can Increase the Security of Your Software
There is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: is it the specification phase or the…
Fabien Chouteau, Yannick Moy, Vasiliy Fofanov, Nicolas Setton
A Modern Syntax for Ada
One of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this…
Yannick Moy
Two Days Dedicated to Sound Static Analysis for Security
AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they…
Yannick Moy
Secure Software Architectures Based on Genode + SPARK
SPARK user Alexander Senier presented recently at BOB Konferenz in Germany their use of SPARK for building secure mobile architectures. What's nice…
Yannick Moy
Tokeneer Fully Verified with SPARK 2014
Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran…
Yannick Moy
For All Properties, There Exists a Proof
With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to…
Pierre-Marie de Rodat, Yannick Moy, Fabien Chouteau, Raphaël Amiard
AdaCore at FOSDEM 2018
Yannick Moy, Martin Becker, Emanuel Regnath
Physical Units Pass the Generic Test
The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue…