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



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
-- 
David MENTR? - Research engineer, Ph.D.
   Formal Methods and tools
MITSUBISHI ELECTRIC R&D Centre Europe (MERCE)
Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59
http://www.fr.mitsubishielectric-rce.eu
-------------- next part --------------
A non-text attachment was scrubbed...
Name: introduction-to-frama-c_v1.pdf
Type: application/x-download
Size: 515076 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130903/f6c63818/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: introduction-slides-examples.tar.gz
Type: application/x-gzip
Size: 2732 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130903/f6c63818/attachment-0003.bin>