Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] New release of "ACSL by Example"
  • From: jens.gerlach at first.fraunhofer.de (Jens Gerlach)
  • Date: Sun, 13 Feb 2011 20:38:01 +0100
  • References: <EFF6534C8F2FC940A9D7929433E12D4E3A64FF@TITAN.first.fraunhofer.de>
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