--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New release of "ACSL by Example"



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