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

[Frama-c-discuss] Generation of invariants




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                    |