--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on September 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example (version 15.1.1 for Frama-C 15 (Phosporus))



Dear Frama-C users,

The Verification Group at Fraunhofer FOKUS has released a new version (15.1.1) of “ACSL by Example”.
This version is intended for Frama-C 15 (Phosporus).
Its source can be accessed through Github

            https://github.com/fraunhoferfokus/acsl-by-example

The PDF document can be directly accessed through

            https://github.com/fraunhoferfokus/acsl-by-example/blob/master/ACSL-by-Example.pdf

There are no new algorithms in this release.
The most notable changes are

- rewrite axiomatic definitions to ensure disjoint guards which is better suited for E-ACSL
- shorten names of some auxiliary algorithms
- heap algorithms

   * fix typos in two heap figures
   * explain that there can be multiple representations of an array as a heap
   * add a version of pop_heap that is, however, not completely verified

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

Regards

Jens Gerlach

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170919/3c5c95df/attachment-0001.html>