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] Aluminium release of "ACSL by Example"

  • Subject: [Frama-c-discuss] Aluminium release of "ACSL by Example"
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Mon, 8 Aug 2016 12:32:34 +0000
Dear Frama-C users,

116 years ago today (8. August) the mathematician David Hilbert presented in the Sorbonne 23 problems (https://en.wikipedia.org/wiki/Hilbert%27s_problems).
His second problem had a huge influence on the research on mathematical logic and through this also on formal methods 
for computer science.

Thus, 8. August is a nice day for the Verification Group at Fraunhofer FOKUS to release a new version of “ACSL by Example”.
This document has been updated for the Aluminium release of Frama-C and can be accessed through 

          http://www.fokus.fraunhofer.de/download/acsl_by_example

The most notable changes of this version, besides the the updates for the Aluminium release of Frama-C, are

	- the re-introduction of heap algorithms. 
          This new description of heap algorithms is based to a large extend  on the bachelor thesis of Timon Lapawczyk.

        - verification of a more efficient implementation of equal_range

        - the addition of the new algorithms search_n and remove

        - the simplification of loop annotations of remove_copy

We hope this document helps you in your work with Frama-C/WP.

Regards

Jens Gerlach