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
- Prev by Date: [Frama-c-discuss] [wp] user error: Can not create output directory '/tmp/wpd596aa.dir/typed'
- Next by Date: [Frama-c-discuss] frama-clang build error
- Previous by thread: [Frama-c-discuss] Frama-c-discuss Digest, Vol 98, Issue 1
- Next by thread: [Frama-c-discuss] frama-clang build error