--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Timed properties



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