Email Gateway (Aug 22 2022 at 16:26): Email Gateway (Aug 22 2022 at 16:26):From: Li Yongjian <lyj238@gmail.com>
Dear Isabelle experts:
Why3 is a platform for deductive program verification. It provides a
rich language for specification and programming, called WhyML, and relies
on external theorem provers, both automated and interactive, to discharge
verification conditions.
I want to know whether Isabelle has been used to discharge
verification conditions of why3? or someone has related Isabelle with why3?
regrads!
yongjian Li
Email Gateway (Aug 22 2022 at 16:26):From: Claude Marché <Claude.Marche@inria.fr>
Hello
Le 20/11/2017 à 22:53, Li Yongjian a écrit :
Dear Isabelle experts:
Why3 is a platform for deductive program verification. It provides a
rich language for specification and programming, called WhyML, and relies
on external theorem provers, both automated and interactive, to discharge
verification conditions.
Right, it is the official short description for Why3, Indeed.
I want to know whether Isabelle has been used to discharge
verification conditions of why3?
Yes, Isabelle/HOL is one of the supported back-end prover. See however
the specific doc section http://why3.lri.fr/doc/itp.html#sec114 for the
special things to do to use Isabelle/HOL from Why3
or someone has related Isabelle with why3?
Stefan Berghofer is the person who contributed most of the Isabelle
support in Why3, and probably the one who made the most complex proofs
using Why3+Isabelle.
Hope this helps,
Last updated: Apr 23 2024 at 12:29 UTC