2 ms·

Thanks, interesting example! Interestingly, http://compcert.inria.fr/release/Changelog http://compcert.inria.fr/release/Changelog mentions various "bug fixes"

Thanks, interesting example! Interestingly, http://compcert.inria.fr/release/Changelog http://compcert.inria.fr/release/Changelog mentions various "bug fixes" in almost every release, and the mentions of "successful tests" are not quite canonical either, but it certainly looks like a successful, nontrivial program.

gsg 15y ago
Yes, CompCert is no timeless perfect gem. You could make a convincing argument that it's not really verified software in the Djikstra mold at all (only parts of the compiler are verified, although they are fairly large and interesting parts). It does make a nice poster child for formal methods though.