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] Simplify prover instalation problem


On 05/10/15 04:47, Allberson Dantas wrote:
> Dear David, do you know some publication that highlights these things
> that differ each prover from the others in Why3? For example, from the
> characteristics of the program, how to choose the best prover (SMT, TPTP
> or dedicated) would be the best.

I think there is no unique best prover for a given program, but there is
a best prover for each single verification condition of a program. This
is why I repeat, again and again, that a user should install as many
provers as she/he can, and try to run each prover on each VC.

There is the interesting question on how to predict, from the shape of a
VC (e.g. the root predicate of the conclusion), what are the provers
that are more likely able to discharge it. I cannot recommend any paper
on that, I think it is an interesting and difficult open problem.

- Claude





-- 
Claude March?                          | tel: +33 1 69 15 66 08
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |