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

Hello Benjamin,

2011/2/1 MONATE Benjamin 205998 <Benjamin.MONATE at cea.fr>:
> Thanks a lot for making your slides available: they provide a nice and precise overview of two plugins of Frama-C.

Thanks.

> What kind of remarks/questions did you get?

Regarding Value analysis (also presented in another lesson): mostly
questions regarding lack of precision on values, especially regarding
loops (and "all programs are loops", quoting a participant). I talked
about the skein analysis in Value analysis tutorial which is able to
provide some interesting result and the use of -slevel. But I lack
first hand practice on applying value analysis to large code. Is it a
real issue on control code, for example?

Regarding Jessie: "annotations have the same size as code!" and "what
about error in annotations?". For the former remark, I could only tell
that this was the price to pay to be able to *prove* code in all its
generality. Regarding the latter remark, I told it would not be
possible to prove the goals, but a was lacking convincing arguments.
One of the attendee followed a lesson on code proof using a functional
approach and PVS powerful tactics made by a researcher at INRIA Rennes
(Thomas Genet) and told the approach was more powerful and simple. I
answered that the discussion between the two approaches is still
on-going. :-)

Overall, I already asked for it but having some examples (or better an
article that could be cited!) detailing how Frama-C is applied on some
industrial code (size of code, most important issues and approaches
used to work around them, results obtained) would be very useful.

Sincerely yours,
david