--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C ACSL examples



Hello,

2015-05-29 16:10 GMT+02:00 V?tor Alcantara de Almeida
<vitoralcantara at ppgsc.ufrn.br>:
> someone has available examples of annotated  C code or could inform where I
> can find them, specially examples that weren't successfully proved.
>

- The wiki contains material from various tutorials
https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:tutorial.
A certain number of them have code examples with ACSL specifications
to be validated by WP.
- The Toccata team from Inria maintains a gallery of verified
programs, including some verified with Frama-C:
http://toccata.lri.fr/gallery/frama-c.en.html

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile