AdaCore Blog

Research Corner - SPARK 2014 vs Frama-C vs Why3

by Yannick Moy

There have been informal comparisons by researchers between the use of SPARK and Frama-C, but these are not enough to really understand the most important differences at the heart of the these different toolsets for formal verification of programs. Another interesting point of comparison is the Why3 technology which underlies both SPARK 2014 and Frama-C (when using the Jessie plugin instead of the WP plugin for deductive verification). Hence the interest of this article we have written for the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, which goes into deeper difference in design choices between these technologies, in terms of executability, semantics of logical parts, use of ghost code, and generation of counterexamples.

Posted in #Formal Verification    #SPARK   

About 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 Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.