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