--- layout: fc_discuss_archives title: Message 81 from Frama-C-discuss on October 2008 ---
Hi, Note that this plug-in is experimental (and its documentation too). Hence, if you have any specific problem or question about this plug-in or its usage, don't hesitate to write me. Nicolas. Claude March? a ?crit : > > Hi, > > I'm not sure I understand what you are your objectives. You should have > a look at a new plugin "ltl to acsl" which will be distributed in the > next Frama-C release. Then, comments and discussion on this list will be > welcome. > > - Claude > > Nickolay V. Shmyrev wrote: >> Hi all >> >> I'm going to try to build some extended example of frama-c with proof of >> LTL properties, probably realtime properties, and probably some runtime >> check integration. Also I'd like to build an example proof of validation >> of the code and model, say validation for an automata model. >> >> As far as I see now I should extend axioms and write some logic as well. >> >> Do you think it's something doable? >> >> >> >> >> ------------------------------------------------------------------------ >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss@lists.gforge.inria.fr >> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- section suivante -------------- Une pi?ce jointe non texte a ?t? nettoy?e... Nom: nicolas_stouls.vcf Type: text/x-vcard Taille: 469 octets Desc: non disponible Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081020/6ff36932/nicolas_stouls.vcf