--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



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