--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on July 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL by Example and automatic provers



Hi,

Le 18/07/2017 12:53, Gerlach, Jens a écrit :
> I don’t think we had a bias towards Alt-Ergo because for a long time we
> have used CVC4 and Z3 in our
> verification pipeline before Alt-Ergo.
>
> I suspect, however, that the Alt-Ergo development follows WP and Why3
> more closely than the other provers.

Actually, the WP plug-in has a dedicated Alt-Ergo output, while it 
relies on Why3 for the other provers. It may explain Jens's results.

--
Julien