Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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                    |