--- layout: fc_discuss_archives title: Message 81 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,

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