[Verifpal] Verifpal for academic formal verification?
renaud.lifchitz at gmail.com
Thu Sep 12 13:25:39 CEST 2019
Wonderful, thanks for these insights.
Keep up the good work!
Le jeu. 12 sept. 2019 à 12:42, Nadim Kobeissi <nadim at symbolic.software> a
> Longer answer in which I address related questions:
> A. Why release Verifpal before the soundness proof was done?
> 1.Because a soundness proof doesn't equal a bug-free implementation.
> 2. Because I don't want to prove secure a language that we then realize
> could be changed and improved with user feedback (as has already occured),
> thereby requiring another proof.
> B. Is it worth learning Verifpal before the soundness proof comes out?
> Absolutely. The language won't change, the feature set won't change. The
> skillset and capabilities that learning Verifpal today or next year will
> remain constant, and I recommend people get involved early on so I can get
> a better understanding of how to direct the project and its formalizations.
> The only thing that will change once the soundness result is out (and
> translated to the implementation of Verifpal itself) is that you'll be more
> sure of Verifpal not missing attacks.
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
> Sent from my phone
> On Thu, Sep 12, 2019, 12:34 PM Nadim Kobeissi <nadim at symbolic.software>
>> Dear Renaud,
>> This is the current major research goal for Verifpal and is underway,
>> with a planned publication for early 2020.
>> Nadim Kobeissi
>> Symbolic Software • https://symbolic.software
>> Sent from my phone
>> On Thu, Sep 12, 2019, 12:11 PM Renaud Lifchitz via Verifpal
>> <verifpal at lists.symbolic.software> wrote:
>>> Hi Nadim,
>>> Thanks again for your very active contribution to the project.
>>> Do you have a roadmap or a timeline for when it could be used for
>>> academic formal verification work like ProVerif?
>>> Is it planned or will it stay like now for training/education mostly?
>>> Thank you.
>>> Best regards,
>>> Renaud Lifchitz
>>> Verifpal mailing list
>>> Verifpal at lists.symbolic.software
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Verifpal