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

[Frama-c-discuss] ACSL by Example (new release 7.1.1)



Dear Frama-C users,

the Verification group at Fraunhofer FOKUS (formerly Fraunhofer FIRST) is pleased to announce 
a new release of our "ACSL By Example" document.
You can download it through

    http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf

(We ask you to update your url in case you maintain a link to our tutorial.)

Many thanks to Yannick Moy from AdaCore who suggested many clarifications and improvements.
A more detailed description of the changes can be found in appendix A of the document.

We also wish to thank our Device-Soft project partners from CEA LIST for their strong support.
More information on Device-Soft can be found under

   http://www.fokus.fraunhofer.de/en/quest/projekte/abgeschlossene_projekte/device_soft/index.html

We have used the Nitrogen release of Frama-C/WP together with alt-ergo to verify our examples. 
The verification results are presented in Chapter 9.

We plan to update this document when a new Frama-C release arrives.


Best regards

Jens Gerlach