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