Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Arbitrary size fixed integer math

Hello Kurt ,

Le 25/10/2015 18:19, Kurt Roeckx wrote :
> On Sun, Oct 25, 2015 at 06:05:09PM +0100, Pascal Cuoq wrote:
>> On Sat, Oct 24, 2015 at 2:04 PM, Kurt Roeckx <kurt at roeckx.be> wrote:
>>
>>> I was wondering if it would be possible to verify the math of the
>>> BN library in OpenSSL. So I tried a little test program to see
>>> what would happen.
>>>
>> Your simplified program is definitely in scope for the deductive
>> verification plug-ins WP and Jessie, and I say this with the serenity of
>> one who does not have access to these tools today and is only going to
>> provide vague hints and guesses throughout this message.
> Thanks for all the hints, I'll know what to try next and let you
> know what works and doesn't work.
>
Yes, it is in the scope for deductive verification, but it may need
significant work of formalization and axiomatization about
decomposing numbers in a base (and re-composing them)
to prove the correctness of a such library.

Patrick.