--- layout: fc_discuss_archives title: Message 33 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



Hi David,

That's a nice work. It could be put somewhere on the Frama-C wiki: on 
the tutorial page? 
(http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial)

--
Julien

On 09/03/2013 03:27 PM, David MENTRE wrote:
> 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
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss