--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2009 ---
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, on the subject of inferring probable invariants (that are checked, e.g. through automatic theorem proving). Get it from: http://www.lri.fr/~moy/publis.html As far as I remember, his technique relies on abstract interpretation, with linear relational abstract domains (his implementation in Jessie uses the APRON library). What makes his approach interesting is that the variables for which relations are inferred are not only the variables of the program but also quantities that are implicitly manipulated by the program, such as the offset of the current value of a pointer with respect to its original value. The design space for the automatic inference of invariants is very large and there are lot of possibilities in terms of research as well as for the application of the existing ideas that look promising. Thanks for considering Frama-C. We would be glad to see new plug-ins appear outside from ours. In fact, the next release will give external plug-ins first class citizenship: for most architectures, it will become possible for someone interested in your plug-in to use it without having to recompile eir[1] existing version of Frama-C. Pascal [1] http://en.wikipedia.org/wiki/Spivak_pronoun