--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on February 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] 'ACSL by Example' for Magnesium



Dear Frama-C Users,

Fraunhofer FOKUS has just provided an updated version of  “ACSL by Example”.
The new version 12.1.0 which is intended for Frama-C Magnesium can be downloaded  through 

	http://www.fokus.fraunhofer.de/download/acsl_by_example

The sources can be accessed through the public git repository 

	https://gitlab.fokus.fraunhofer.de/verification/open-acslbyexample.git

This version contains three new functions and couple of other changes

	- ‘replace’ 					which replaces a value in an array by another one
	- ‘partial_sum_inverse’			which verifies that applying ‘adjacent_difference' after ‘partial_sum' produces the original array
	- ‘adjacent_difference_inverse’	which verifies that applying ‘partial_sum' after ‘adjacent_difference' produces the original array

A main goal of this release was to reduce the number of proof obligations that cannot be verified automatically 
and therefore must be tackled by an interactive theorem prover such as Coq.
To this end, we analyzed the proof obligations (often using Coq) and devised additional assertions or ACSL lemmas to 
guide the automatic provers.

Often we succeeded in enabling automatic provers to discharge the concerned obligations.
Specifically, whereas the previous version 11.1.1 of
'ACSL by Example' listed 9 proof obligations that could only be discharged with Coq, the current version 12.1.0
only counts 5 such obligations.
Moreover, all these remaining proof obligations are associated to ACSL lemmas, which
are usually easier to tackle with Coq than proof obligations directly related to the C code.
The reason for this is that ACSL lemmas usually have a much smaller set of hypotheses.

Adding assertions and lemmas also helps to alleviate a problem in Frama-C Magnesium (and Sodium) where prover 
processes are not properly terminated (see BTS entry 2145).
Left-over ``zombie processes'' lead to a deterioration of machine performance which sometimes results in unpredictable 
verification results.

Regards

Jens Gerlach

Head of Verification Group
Fraunhofer FOKUS
Berlin, Germany