Interestingly, 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.
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.
Comments
Thanks, interesting example!
Interestingly, 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.
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.