--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] New version of ACSL by Example



Dear Frama-C users,

the verification group at Fraunhofer FOKUS has provided a new version of ?ACSL by Example?.
You can download it from http://www.fokus.fraunhofer.de/download/acsl_by_example

The examples have been verified with the Neon release of Frama-C/WP.
- We have added more predicates in order to make our specifications more expressive (and concise).
- In the previous version some proof obligations of three algorithms (equal_range and the
  two version of remove_copy) had to be verified with Coq.
  Now we have to resort to Coq only for some proof obligations of the second version of remove_copy. 

The changes are described in more detail in Section 1.1.

Regards

Jens Gerlach