[Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
Dillon.Pariente at dassault-aviation.com
Tue Feb 1 14:09:33 CET 2011
All these different points of view are very interesting, and sometimes
far from what we do "in-house" with Frama-C.
So I hope this short message will also contribute to enlarge any
newcomer's vision of the possible usages of the platform.
In our industrial experiments, we use different Frama-C plug-ins, mainly
Value Analysis and WP (1). Both have their own advantages and drawbacks.
Either due to their underlying methods, or their implementations. It's
true that Abstract Interpretation with Value Analysis (or certainly
other tools of the same kind!) may lead to non-conclusive
over-approximations wrt to the sought properties, or may be sometimes
too much time-consuming. It's also true that Proof of Program needs a
lot of annotations to obtain sometimes apparently "straightforward"
proofs of properties.
Fortunately, for *our* purpose (I do insist to avoid any misleading
generality: for our classes of C codes and properties addressed in our
use cases), these good and bad "points" do compensate one each other ...
of course, only if the two approaches (Value Analysis and WP) are used
Briefly, Value Analysis, as a context-sensitive analyzer, is from our
point of view very well adapted to deal with a whole application
analysis. When some analyzed C functions lead to too much time-consuming
during their analysis, or if Value Analysis yields a non-conclusive
over-approximation of these functions' outputs, then it is time to use a
weakest-precondition approach (with WP or Jessie plug-ins). ACSL
annotations will alleviate Value Analysis charge and improve its
precision, and later on, will be discharged by WP (or Jessie).
These two approaches are, on the basis of our lessons learnt on real
industrial codes (on large parts generated from synchronous data-flow
models (2)), definitely complementary. Value Analysis is a powerful
tool, able to obtain "sufficiently" accurate results in a small amount
of time (analysis on our codes are between 15 minutes and 1 hour).
Annotations needed to help Value Analysis in obtaining this "sufficient"
accuracy, are not so numerous (in comparison with the workload that
would be necessary to do the whole job only by means of a deductive
As most of these annotations are asserts or quite simple statement
contracts, i.e. "close" to the instructions that will be used to build
the related proof-obligations, they can be discharged ... "almost"
(1) We also used Jessie in previous experiences.
(2) A link in Frama-C publications page will point to our FoVeOOS'10
paper for more details.
More information about the Frama-c-discuss