[Verifpal] Verifpal for academic formal verification?

[Renaud Lifchitz]

Wonderful, thanks for these insights.

Keep up the good work!


Best regards,

Renaud Lifchitz

Le jeu. 12 sept. 2019 à 12:42, Nadim Kobeissi <nadim at symbolic.software> a
écrit :

> 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>
> wrote:
>
>> 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
>>> https://lists.symbolic.software/mailman/listinfo/verifpal
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190912/4c0eeb96/attachment.htm>