--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on May 2015 ---
[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                    |