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

[Frama-c-discuss] RE : Loop invariants with imbricated loops.



Hi,

Thanks for your full z3 howto. It probably needs to be written to the Wiki on http://bts.fram-c.com.

As esc/java2, AFAIK the associated prover is Simplify and they intend to use other SMT provers.
So which prover do you have in mind? In any case support for new provers is a feature request for Why itself.

Cheers,
--
Benjamin Monate
CEA LIST
Head of Software Safety Lab.

-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: non disponible
Type: application/ms-tnef
Taille: 2926 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090520/c881584d/attachment-0001.bin