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



The jessie plugin is able to prove that a C function satisfy a given
invariant (written with ACSL).

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.

Currently, I'm taking a look at the approach proposed by
Rodriguez-Carbonell1 and Kapur:
http://cat.inist.fr/?aModele=afficheN&cpsidt=16144026
http://www.springerlink.com/content/rg4l1e1l996eulja/
http://portal.acm.org/citation.cfm?id=1222241.1222597