--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on May 2015 ---
On Sat, 9 May 2015 23:47:13 -0300, Allberson Dantas <allberson85 at gmail.com> 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. > > Thanks a lot. > > 2015-05-02 12:28 GMT-03:00 David MENTR? <dmentre at linux-france.org>: > > > Hello, > > > > Le 2015-05-01 20:38, Allberson Dantas a ?crit : > > > >> I've seen in a frama-c tutorial that simplify, even being discontinued, > >> is the most powerfull prover to deal with frama-c. > >> > > > > I doubt there is such thing as "the most powerfull prover". Provers are > > good for one thing and bad for others. Nowadays, CVC4, Z3 or Alt-Ergo have > > pretty good reputations. > > > > You'd rather go for supported one. I agree that different provers are good at different things, and that CVC4, Z3, and alt-ergo have great reputations. That said, one advantage of "Simplify" is that it works in a *completely* different way from most other provers. As a result, it has a chance of succeeding when others do not. Historically Simplify did a good job with a lot of expressions. One problem with Simplify is that it was not originally released under an open source software (OSS) license. I asked, and HP agreed to release Simplify under a GPLv2+ license; that is noted here: http://www.dwheeler.com/misc/simplify-hp-release.txt Sadly, by the time I got that info, I had moved on to other things, but that release may help others restart support for Simplify. If that happens, please let me know. --- David A. Wheeler