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] Introductory slides on Frama-C

Hi to all,

A few remarks from me, without mathematics:

slide 5: I don't think it is accurate to attach the term "formal
methods" to only abstract interpretation and deductive verification. I
don't think the spectrum of "formal methods" is that well defined,
indeed from my point of view the simple concept of using a computer
program to analyse another computer program is already a "formal
method", and in that sense all Frama-C plugins belong to formal methods.
For example, there is a research area called "formal testing". But
anyway, you could use "static analysis" to group abstract interpretation
and deductive verification. "Specification generation" could belong to
"static analysis" too.
See also http://www.fmeurope.org/, where even if the term is not very
clearly defined, it is obviously not limited to static analysis.

slide 7: I don't think Jessie is already "deprecated". Jessie3 simply
does not exist, even if it may exist in some future.

slide 9: probably more accurate is Why in 2001 and Caduceus 2004 (but
who cares...)

slide 10: a bit frightening, don't you think? First things one needs are
tutorials (including yours) and illustrative examples, no?

slide 24: Everything should be proved to "assume correct program"?
shouldn't it be to "guarantee the program correct" ?

slide 27: No ?IF p THEN q1 ELSE q2? ? But according to ACSL manual, one
may write (p ? q1 : q2). (May be it is not implemented...)



Le 03/09/2013 15:27, David MENTRE a ?crit :
> In slide 47, behaviours found and not_found have opposite logical
> condition for assumes clauses. However I find difficult to explain it
> without going back to first order logic (!(a ==> b) eq. !(!a || b) eq.
> ...) which I would like to avoid. Any idea on a way to explain that simply?

Though question indeed... using ==> instead of && after \exists is an
frequent mistake...

- Claude

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |