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

[Frama-c-discuss] ACSL by Example (version 15.1.2 for Frama-C 15, Phosphorus)



Dear Frama-C users,

The Verification Group at Fraunhofer FOKUS has released a new version (15.1.2) 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

- In this release we discuss the formal verification of three (classic) sorting algorithms:
   selection_sort, insertion_sort and heap_sort.

- We have fixed many typos, some of which have been reported by 
  the GitHub user ‘seniorlackey’ (thanks a lot!).

- We have also improved the description of various algorithms, notably the heap algorithms
  push_heap and pop_heap.

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

Regards

Jens Gerlach