--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2009 ---
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