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

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

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |