--- layout: fc_discuss_archives title: Message 20 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 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