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