--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on May 2009 ---
Pascal Cuoq wrote: > Hello, > > On May 4, 2009, at 12:22 PM, Jonathan-Christofer Demay wrote: > >> Another thing I would be interested in is quite the opposite. Given >> a C >> function, I would like to compute an invariant at a particular point >> of >> a function. >> >> I this something that has already been thought of as futur feature of >> Frama-C ? If not, well then this is something I'm considering working >> on. > > You may be interested in Yannick Moy's article at VMCAI 2008, A more recent and more detailed reference than "eir" VMCAI paper is "eir" thesis: http://www.lri.fr/~marche/moy09phd.pdf > [1] http://en.wikipedia.org/wiki/Spivak_pronoun -- 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 |