--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2016 ---
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