3 ms·

One of their compilers is never wrong: "Formal Methods as Bugscreen [--] the formally-verified CompCert compiler"

• jcranmer 7y ago
  John Regehr did find 11 bugs in CompCert (the unverified portion).
  • tuukkah 7y ago
    If I've understood correctly, the compiling step is verified but the parsing and assembly steps are not, and no bugs have been found where valid input would have been compiled to valid but wrong assembly. I didn't see a statement about this on CompCert's web site though.
• setr 7y ago
  There were no bugs that their program could find; not that there are no bugs at all :-)