Yannick Moy

Yannick Moy’s work focuses on software source code analysis, mostly to detect bugs or verify safety/security properties. Yannick previously worked for PolySpace (now The MathWorks) where he started the project C++ Verifier. He then joined INRIA Research Labs/Orange Labs in France to carry out a PhD on automatic modular static safety checking for C programs. Yannick joined AdaCore in 2009, after a short internship at Microsoft Research.

Yannick holds an engineering degree from the Ecole Polytechnique, an MSc from Stanford University and a PhD from Université Paris-Sud. He is a Siebel Scholar.

What does Frontline Support mean to you?

Making sure that a customer experiencing a problem receives the best possible answer very fast. It is a collaborative process in which we learn a lot. For example, it is quite common that one of us expands on an answer provided by someone else.

What drew you to Ada?

My experience working on the PolySpace C++ Verifier teached me that a really useful source code analyzer should be able to automatically analyze a piece of code in isolation but still benefit from some user input if provided. These features are also known as modularity, automation and user interaction. These are all the things you find in a compiler! AdaCore is on the way to make the “verifying compiler” dream more real. To that end, the joint work we have started at AdaCore, Praxis and SofCheck is really pioneering the combination of verification tools that are needed in practice: the GNAT compiler of course, the CodePeer static analyzer and the SPARK proof tools.

Now, tools are a poor replacement for a well-defined language which gives programmers the ability to specify many fine-grain properties. Ada is way above any mainstream curly-brace language when it comes to this power of expressing fine-grain properties: in-out parameters, integer ranges, memory pools and non-null pointers are just a few examples of fine-grain properties that must be recovered in other languages with expensive and incomplete source code analyses. Did I tell you that the next version of Ada will include contracts and invariants?

What’s your favorite feature of GNAT Pro Technology?

Industrial state-of-the-art free software tools. A great combination.

Of course, I have a preference for our source code analyzers. They are the future of tests. Tests will always play a critical part, if only because only good programmers survive a test campaign! Like C.A.R. Hoare said in 2009: “I did not realize that the success of tests is that they test the programmer, not the program.” But there will always be bugs and glitches. Tools can help.