--- layout: fc_discuss_archives title: Message 14 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



tor 2018-11-15 klockan 14:23 +0000 skrev Gerlach, Jens:
> 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.)

I sent this so some friends of mine who are verification-curious, and
it gave me some more inspiration for proofs, so this work is very much
appreciated :)

/Tomas