--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on February 2011 ---
[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