--- layout: fc_discuss_archives title: Message 79 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Memory model



Hi,

Francois Dupressoir wrote :
> It also seems that Frama-c's plugin architecture would be good for our 
> rather specific purpose verification problems, as opposed to having to 
> give annotations that are not relevant to our goals.

I don't know what you have in mind, but I would like to inform you
that we are currently working on a WP computation that may use
several memory models. This work is in a very experimental stage,
so it is difficult to say much on it, except that it is going on...

> I will keep you informed of anything I implement, and you will probably 
> get more questions from me in the future :)

Great : we are looking forward to here from you !

Regards,

Anne.
-- 
Anne Pacalet  -
INRIA - 2004, route des Lucioles BP.93 F-06902 Sophia Antipolis Cedex.
Tel : +33 (0) 4 9715 5345