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] Verification of linked list

  • Subject: [Frama-c-discuss] Verification of linked list
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Tue, 10 Mar 2015 14:37:50 +0000
  • In-reply-to: <mailman.29.1425985217.7479.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.29.1425985217.7479.frama-c-discuss@lists.gforge.inria.fr>

> You should take a look at "ACSL by Example" from Fraunhofer FOKUS:

Thanks for referring to our document, David!
Here is the shorter, official URL to ?ACSL by Example?:

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

But I have to point out that its examples are much simpler than linked lists?

> PS @Jens: finding the PDF file is always difficult. ;-) You should put 
> it on a simple web page or attached to a blog entry.
> 

I agree, but our PR likes to shuffle our web pages from time to time.
Nothing much I can do here.
The problem is also, that older copies of ACSL by Example are at different locations in the web.

A good idea is to look at the the wikipedia page for ACSL 
http://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language

In the References section (http://en.wikipedia.org/wiki/ANSI/ISO_C_Specification_Language#References)
there is a link to the most recent version of ?ACSL by Example?.

Jens