Formal verification with cbmc

[marco.bodrato at tutanota.com]

Ciao Niels!
1 gen 2026, 16:22 da nisse at lysator.liu.se:

> I wonder if anyone on this list has experience with formal verification,
> or cbmc (https://www.cprover.org/cbmc/) in particular?
>
I don't.

But I remember that I saw some interesting papers about formal verification of the implementation of some functions of GMP.

One is 20 years old, by Paul Zimmermann et al., they used Coq.
https://inria.hal.science/inria-00072113v1/file/RR-4475.pdf

A fresher couple of papers, by Raphaël Rieu-Helft et al., used Why3.
https://jfr.unibo.it/article/view/9730
https://inria.hal.science/hal-01699754v2

I personally do not even know if "Coq", "Why3" and "cbmc" are somehow comparable or their point of view is completely different. But it would be interesting to know which framework may be more suitable to verify such a complex library, with the focus on big numbers.

> Regards,
> /Niels
>
Ĝis,
m