--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on September 2012 ---
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