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

[Frama-c-discuss] ACSL by Example (version 21.1.1)



Dear Frama-C users,

Fraunhofer FOKUS has just released a new version (21.1.1) of “ACSL by Example”.
This version is intended for Frama-C 21.1 (Scandium).
The examples 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

In this version we have particularly improved the annotations and documentation of the following algorithms
   - push_heap
   - pop_heap (verified finally the postcondition ‚reorder‘)
   - merge

Please refer to the changes section for a more detailed description.
We would particularly like to thank Jochen Burghardt for his comments on the push_heap and pop_heap!

We hope that this version helps you in learning and applying Frama-C/WP!

Jens Gerlach