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 4.2.1 released

  • Subject: [Frama-c-discuss] ACSL by Example 4.2.1 released
  • From: jens.gerlach at (Jens Gerlach)
  • Date: Tue, 6 Apr 2010 15:51:18 +0200

The DEVICE-SOFT team at Fraunhofer FIRST is pleased to announce the  
of the "ACSL by Example" tutorial, version 4.2.1.

This release offers several improvements and fixes.
The following enhancements are included in version 4.2.1:

- an alternative speci?cation of the remove_copy algorithm that uses  
ghost variables
- added a new chapter, Chapter 5 on heap operations
- added the STL mismatch algorithm (Section 3.2)
- moved algorithms adjacent_find and min_element from the appendix to  
Chapter 3
- added typedefs size_type and value_type and used them in all  
- renamed is_valid_int_range to is_valid_range

The tutorial can be downloaded directly through the following link:

Some readers have asked whether they can use this tutorial in a  
As long as you follow the license conditions ( 
on page 2 of the tutorial we see no problem using this tutorial for  
In fact, we would be very happy if our tutorial helps you adopt the  
usage of formal methods.

For more information on the DEVICE-SOFT project please refer to our  
project page


Jens Gerlach


Dr.-Ing. Jens Gerlach
Eingebettete Systeme - EST
Tel.: +49 (0)30 6392 1841
Fax.: +49 (0)30 6392 1805
E-Mail: jens.gerlach at

Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST
Kekul?stra?e 7
12489 Berlin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>