--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on March 2015 ---
Dear all, There is already work done on the verification of kLIBC, which was published last year: link <http://link.springer.com/chapter/10.1007%2F978-3-319-06200-6_29> (public copies are available, look for it) The public repository with annotated code can be found here <https://github.com/Beatgodes/klibc_framac_wp>. Kind Regards, Cristiano Sousa David R. Cok <dcok at grammatech.com> escreveu no dia qui, 19/03/2015 ?s 14:37: > I echo this inquiry. > > In addition, if any group would like to participate in (use and > contribute) a public repository of ACSL annotations on widely used > libraries - as we are - , please respond to this group. > > There are of course issues to work out. There are logistical issues such > as hosting location and copyright releases. There are also scientific > issues such as whether a common set of annotations can be widely used for > multiple tools and multiple applications. > > > - David > > > On 3/18/2015 2:55 PM, Andre Oliveira wrote: > > Dear all, > > It has been mentioned during the Frama-C day that better ACSL > specifications concerning the standard C library would be useful to the > platform. > > I would like to find out about existing public repositories with such > specifications, to have an idea of the kind of specifications that are > used, and also their level of detail. > > An example would be kLIBC, a subset of the C standard library with an > annotated implementation. I am also interested in pure specifications, > without an underlying implementation. > > > Regards, > Andr? Oliveira > > > _______________________________________________ > Frama-c-discuss mailing listFrama-c-discuss at lists.gforge.inria.frhttp://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > > _______________________________________________ > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150319/d1566215/attachment.html>