--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on February 2011 ---
Dear Frama-C Users, as part of the DEVICE-SOFT project of CEA LIST and Fraunhofer FIRST, we have released a new version of "ACSL by Example". The document can be downloaded from http://www.first.fraunhofer.de/device_soft_en Major changes are the inclusion of binary search algorithms and a chapter on the formal verification of a simple data structure ("stack"). A more complete list of changes is included in the document. This release has been targeted for the Boron version of Frama-C/Jessie (http://frama-c.com/jessie.html). However, we have already included some changes (e.g. loop variant must appear after the loop invariants) required by the WP plugin (http://frama-c.com/wp.html) of Carbon. Please contact me if you have questions or suggestions. Regards Jens Gerlach