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] a closer look on std::unique_copy

  • Subject: [Frama-c-discuss] a closer look on std::unique_copy
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Thu, 15 Nov 2018 14:23:03 +0000
Dear Frama-C users,

the team of “ACSL by Example” has written a technical report where we look in some detail on various aspects of testing and formal verification
the algorithm “unique_copy” from the C++ standard library.
(Of course, for the purpose of verification with Frama-C/WP, we had to look at an re-implementation of this algorithm in C.)

This report looks in much more detail on the various aspects of a (simple) algorithm than we have usually done within “ACSL by Example”.
We therefore hope that it provides some useful insights for the Frama-C community.
At the same time we are interested in your feedback (jens.gerlach at fokus.fraunhofer.de)!

The document can be accessed through

   https://github.com/fraunhoferfokus/acsl-by-example/blob/master/VESSEDIA-unique_copy.pdf

This work has been conducted within the Vessedia project (https://vessedia.eu) where this report shall be published as part of a deliverable at
the beginning of next year. (EU regulations require that this document is clearly marked as “draft” before it has been officially accepted.)

Regards

Jens Gerlach

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181115/b79f0b9c/attachment.html>