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

[Frama-c-discuss] "ACSL by Example" for Sodium



Dear Frama-C Users,

Fraunhofer FOKUS has just provided an updated version of  “ACSL by Example”.
The new version 11.1.1 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 a new chapter (7) on numeric allgorithms, in particular, it provided formal specifications of 
the following algorithms

 
	- ‘accumulate’ 			which computes the sum of the elements in a range
	- ‘inner_product’ 		which computes the inner product of two ranges
	- ‘partial_sum’			which computes the sequence of partial sums of a range
	- ‘adjacent_difference’	which computes the differences of adjacent elements in a range

The implementations of these specifications can be verified with Frama-C/Sodium.

Regards

Jens Gerlach

Head of Verification Group
Fraunhofer FOKUS
Berlin, Germany