--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verification of axiomatization



Hello,

On Tue, Apr 7, 2009 at 09:33, Virgile Prevosto <virgile.prevosto at cea.fr> wrote:
> Claude March? <Claude.Marche at inria.fr> a ?crit :
>
>> Another, probably quicker, possibility is first to try to prove
>>
>> //@ lemma l : 0=0;
>>
>
> Shouldn't that be 0!=0 (or 0 == 1)? 0 == 0 is quite easy to prove.

For people new to those issues like me, I would advise to read the
following paper that explains all this in more details:
  A Few Remarks About Formal Development of Secure Systems
  http://arxiv.org/abs/0902.3861

(found in FoCaLize manual)

Yours,
d.