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

  • Subject: [Frama-c-discuss] Generation of invariants
  • From: Pascal.Cuoq at cea.fr (Pascal Cuoq)
  • Date: Mon, 4 May 2009 13:17:26 +0200
  • In-reply-to: <1241432533.21376.122.camel@supelec>
  • References: <1241432533.21376.122.camel@supelec>
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