[Verifpal] Verifpal for academic formal verification?

[Nadim Kobeissi]

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/6c0e0fb6/attachment.htm>