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
- Subject: [Frama-c-discuss] Introductory slides on Frama-C
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Wed, 04 Sep 2013 18:05:45 +0200
- In-reply-to: <5225E3BB.8010903@fr.merce.mee.com>
- References: <5225E3BB.8010903@fr.merce.mee.com>
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 |
- Follow-Ups:
- [Frama-c-discuss] Introductory slides on Frama-C
- From: d.mentre at fr.merce.mee.com (David MENTRE)
- [Frama-c-discuss] Introductory slides on Frama-C
- References:
- [Frama-c-discuss] Introductory slides on Frama-C
- From: d.mentre at fr.merce.mee.com (David MENTRE)
- [Frama-c-discuss] Introductory slides on Frama-C
- Prev by Date: [Frama-c-discuss] Introductory slides on Frama-C
- Next by Date: [Frama-c-discuss] Issues with WP on program doing simplepointer arithmetic
- Previous by thread: [Frama-c-discuss] Introductory slides on Frama-C
- Next by thread: [Frama-c-discuss] Introductory slides on Frama-C
- Index(es):