Ciao Niels! 1 gen 2026, 16:22 da [email protected]: > 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 _______________________________________________ gmp-devel mailing list [email protected] https://gmplib.org/mailman/listinfo/gmp-devel
