Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] 'ACSL by Example' for Magnesium
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Mon, 22 Feb 2016 12:46:27 +0000
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