--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Introductory slides on Frama-C



? 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.