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
SPARK 2014 Rationale: Ghost Code
A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the…
Yannick Moy
Using Coq to Verify SPARK 2014 Code
In the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo. Automatic provers are very handy…
Yannick Moy
Using SPARK to Prove AoRTE in Robot Navigation Software
Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that…
Yannick Moy
Short Video Demo of SPARK 2014
New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!
Yannick Moy
Use of SPARK in a Certification Context
Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification…
Yannick Moy
Contextual Analysis of Subprograms Without Contracts
We have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from…
Yannick Moy
Studies of Contracts in Practice
Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts…
Yannick Moy
GNATprove Tips and Tricks: How to Write Loop Invariants
Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants…
Yannick Moy
Case Study for System to Software Integrity Includes SPARK 2014
My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study…
Yannick Moy
Muen Separation Kernel Written in SPARK
The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been…
Yannick Moy
Rail, Space, Security: Three Case Studies for SPARK 2014
We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014,…
Yannick Moy
GNATprove Tips and Tricks: Referring to Input in Contracts
In a previous post about pre-call values, I described how the Ada language rules implemented in the compiler prevent surprises when referring to…