--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on March 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Standard C library specifications in the wild



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>