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.
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).…
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…
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,…
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,…
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…
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…
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…
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…
Formal Verification of Legacy Code
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…
Ada Lovelace Bicentennial
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…