--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on November 2018 ---
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