--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on November 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] a closer look on std::unique_copy



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>