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.
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…
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,…
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…
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,…
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…
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…
SPARK 2014 Rationale: Loop Invariants
Formal verification tools like GNATprove rely on two main inputs from programmers: subprogram contracts (preconditions and postconditions) and loop…
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…
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…
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,…
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…
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…