--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on October 2008 ---
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? -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 197 bytes Desc: =?koi8-r?Q?=FC=D4=C1?= =?koi8-r?Q?_=DE=C1=D3=D4=D8?= =?koi8-r?Q?_=D3=CF=CF=C2=DD=C5=CE=C9=D1?= =?koi8-r?Q?_=D0=CF=C4=D0=C9=D3=C1=CE=C1?= =?koi8-r?Q?_=C3=C9=C6=D2=CF=D7=CF=CA?= =?koi8-r?Q?_=D0=CF=C4=D0=C9=D3=D8=C0?= Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081018/3e7c881d/attachment.pgp