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

[Frama-c-discuss] ACSL by Example (version 15.1.0 for Phosporus)



Dear Frama-C users,

The Verification Group at Fraunhofer FOKUS has released a new version (15.1.0) of “ACSL by Example”.
This version is intended for Frama-C 15 (Phosporus). 
Starting with this release you the PDF documentation and the examples are hosted at GitHub

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

The document can be directly accessed through

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

The most notable changes of this version are

- The verification results are now part of the appendix.
- Fix an error in the specification of the well-definition of stack_size.
- This release of Frama-C/WP could not discharge some of our assertions of push_heap. 
  We therefore have completely rewritten the annotations and also tweaked the implementation of push_heap. 
  We also added some new predicates and lemmas to maintain a concise specification that can easily be verified by automatic provers.
	* add predicate MultisetAdd and lemma MultisetAddDistinct
	* add predicate MultisetMinus and lemma MultisetMinusDistinct
	* add predicate MultisetRetain and lemma MultisetPushHeapRetain 
	* provide an additional version of predicate MultisetRetainRest
	* and lemma MultisetPushHeapClosure

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

Regards

Jens Gerlach