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: Global State
Global variables are a common source of programming errors: they may fail to be initialized properly, they can be modified in unexpected ways,…
Yannick Moy
SPARK 2014 Rationale: Mixing SPARK and Ada Code
The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification…
Yannick Moy
SPARK 2014 Rationale: Loop Variants
Loop variants are the little-known cousins of the loop invariants, used for proving termination of subprograms. Although they may not look very…
Yannick Moy
SPARK 2014 Rationale: Loop Invariants
Formal verification tools like GNATprove rely on two main inputs from programmers: subprogram contracts (preconditions and postconditions) and loop…
Yannick Moy
SPARK 2014 Rationale: Pre-call and Pre-loop Values
Subprogram contracts are commonly presented as special assertions: the precondition is an assertion checked at subprogram entry, while the…
Yannick Moy
MISRA-C 2012 vs SPARK 2014, the Subset Matching Game
The MISRA C subset of C defines around 150 rules that restrict C programs for critical software development. Of these, 27 rules are classified as…
Yannick Moy
SPARK 2014 Rationale: Specification Functions
Specifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Yet,…
Yannick Moy
SPARK 2014 Rationale: Contract Cases
Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a…
Yannick Moy
Project Hi-Lite Wrap-up
After three years of hard work, we have reached last week the end of project Hi-Lite, whose goal was to simplify the use of formal methods. We're…