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: abiao.yang at gmail.com (David)
  • Date: Wed, 04 Sep 2013 01:52:33 +0800
  • In-reply-to: <mailman.5487.1378215607.1217.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.5487.1378215607.1217.frama-c-discuss@lists.gforge.inria.fr>
? 2013/9/3 21:40, frama-c-discuss-request at lists.gforge.inria.fr ??:
> Send Frama-c-discuss mailing list submissions to
> 	frama-c-discuss at lists.gforge.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
> 	http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
> or, via email, send a message with subject or body 'help' to
> 	frama-c-discuss-request at lists.gforge.inria.fr
>
> You can reach the person managing the list at
> 	frama-c-discuss-owner at lists.gforge.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Frama-c-discuss digest..."
>
>
> Today's Topics:
>
>     1. Introductory slides on Frama-C (David MENTRE)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Tue, 03 Sep 2013 15:27:23 +0200
> From: David MENTRE <d.mentre at fr.merce.mee.com>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: [Frama-c-discuss] Introductory slides on Frama-C
> Message-ID: <5225E3BB.8010903 at fr.merce.mee.com>
> Content-Type: text/plain; charset="iso-8859-1"; Format="flowed"
>
> Hello,
>
> I made some introductory slides on Frama-C. Please find them attached,
> under an open-source licence (CC By-SA 3.0), with C code examples. Feel
> free to re-use them, modify them, etc.
>
> Those slides build on previous slides made by Jochen Burghardt
> (Fraunhofer First), Virgile Prevosto (CEA), Julien Signoles (CEA),
> Nikolay Kosmatov (CEA) and Pascal Cuoq (TrustInSoft).
>
> Compared to those previous presentations, those slides:
>    * Present equally WP and Value analysis;
>
>    * Present behaviors;
>
>    * Present E-ACSL;
>
>    * Avoid any mathematical notation (I am targeting C programmers), many
> thanks to Jochen Burghardt for his slides in that regard.
>
> I tried to present an up-to-date view of Frama-C and its ecosystem.
>
> I would be glad to get any feedback about them: error, things to
> improve, etc.
>
> 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?
>
> Code examples where tested with Frama-C Fluorine.
>
> Best regards,
> david

Nice presentation. Very useful. :-) Thx.