Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie

  • Subject: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
  • From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
  • Date: Tue, 1 Feb 2011 14:09:33 +0100
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F8778E50@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <AANLkTikQfC8Xz4x1CMP=XES-e7a=t-QB8WG1R5Xhex75@mail.gmail.com> <569C6D7D26484241A530B87F45ADE1F8778E50@AOFRWMBXRSC004.resources.atosorigin.local>
Hello,

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
jointly.

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
approach).
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"
easily!

Regards,
D.

(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.