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>
- References:
- [Frama-c-discuss] examples of linked lists or trees
- From: agoodloe at gmail.com (Alwyn Goodloe)
- [Frama-c-discuss] examples of linked lists or trees
- Prev by Date: [Frama-c-discuss] similar assertions not all validated
- Next by Date: [Frama-c-discuss] Postdominators
- Previous by thread: [Frama-c-discuss] examples of linked lists or trees
- Next by thread: [Frama-c-discuss] Postdominators
- Index(es):