--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on October 2015 ---
On Sun, Oct 25, 2015 at 06:05:09PM +0100, Pascal Cuoq wrote: > Hello Kurt. > > 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. Kurt