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 is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents 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.