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] examples of linked lists or trees

  • Subject: [Frama-c-discuss] examples of linked lists or trees
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Wed, 18 Apr 2012 08:02:50 +0200
  • In-reply-to: <CAH5O5PPXWo2Ty8thjurPBjk8fESSMDk0_Xf0r7RVevGtUdy=QQ@mail.gmail.com>
  • References: <CAH5O5PPXWo2Ty8thjurPBjk8fESSMDk0_Xf0r7RVevGtUdy=QQ@mail.gmail.com>
Hi Alwyn,

Verifying programs involving linked list, trees, pointer data structures 
in general, is difficult because
you systematically face issues regarding separation of memory. Known 
solutions in the litterature involve advanced concepts like separation 
logic, ownership, dynamic frames, etc. These need specific specification 
constructs which are not in ACSL. The existing predicate \separated 
supported by WP is not sufficient in general. The internal region 
analysis of Jessie is not sufficient either.

If you want to experiment with a system providing such kind of 
constructs, I recommend Verifast. There are others around of course. 
http://people.cs.kuleuven.be/~bart.jacobs/verifast/

I consider that this subject remains an important topic to study in 
theory, before a simple and satisfactory enough approach will appear in 
a system like Frama-C which aims at industrial applications *now*. Here 
are a few links providing pointer programs examples annotated in ACSL 
and proved in Frama-C (or close)

- In Caduceus, predecessor of Frama-C+Jessie, a few experiments were 
made, including the famous Schorr-Waite a"benchmark" See e.g. Thierry 
Hubert and Claude March? <http://www.lri.fr/%7Emarche/>. A case study of 
C source code verification: the Schorr-Waite algorithm. In Bernhard K. 
Aichernig and Bernhard Beckert, editors, /3rd IEEE International 
Conference on Software Engineering and Formal Methods (SEFM'05)/, 
Koblenz, Germany, September 2005. IEEE Comp. Soc. Press.

- For a recent  study of separation logic concepts in Frama-C, see 
Fran?ois Bobot. /Logique de s?paration et v?rification d?ductive/. Th?se 
de doctorat, Universit? Paris-Sud, December 2011. 
http://tel.archives-ouvertes.fr/docs/00/65/25/08/PDF/VD_BOBOT_FRANCOIS_12122011.pdf

- Claude

On 04/18/2012 05:20 AM, Alwyn Goodloe wrote:
> There are a number of great examples out there off array operations 
> being verified using Jessie or wp. I was wondering if anyone knows if 
> there is a good source of examples of linked list or tree examples.
>
>
> -- 
> Alwyn E. Goodloe, Ph.D.
> agoodloe at gmail.com <mailto:agoodloe at gmail.com>
>
> Research Computer Engineer
> NASA Langley Research Center
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120418/601161b9/attachment.html>