--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on April 2012 ---
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>