--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on October 2015 ---
[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.