--- layout: fc_discuss_archives title: Message 66 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 Claude,
Somehow I haven't seen setup for Z3 prover.
Thanks a lot for notice. To be honest, I have just prepared why - Z3 prover,
for a coming tasks in  project. I didn't try.
Thanks again.
Dragan


On Fri, May 22, 2009 at 12:55 PM, Claude March? <Claude.Marche at inria.fr>wrote:

>
> The wiki already contains a link to the prover tips page of Why.
>
>   http://why.lri.fr/provers.html
>
> Could you elaborate on the difference between your way of using Z3 under
> linux and what is proposed at the Why prover tips page ?
>
> - Claude
>
> MONATE Benjamin 205998 wrote:
> > 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.
> >
> >
> >
> > ------------------------------------------------------------------------
> >
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
> --
> Claude March?                          | tel: +33 1 72 92 59 69
> INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
> Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
> 4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
> F-91893 <http://www.lri.fr/%7Emarche/%0AF-91893> ORSAY Cedex
>      |
>
>
>
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090524/ab397865/attachment.htm