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

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