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: jcdemay at rennes.supelec.fr (Jonathan-Christofer Demay)
  • Date: Mon, 04 May 2009 12:22:13 +0200
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