Formal Verification

From Simson Garfinkel
Revision as of 17:40, 28 May 2017 by Simson (talk | contribs) (Created page with "CompCert is a formally verified optimizing C compiler. "On typical embedded processors, code generated by CompCert typi­cally runs twice as fast as code generated by GCC with...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

CompCert is a formally verified optimizing C compiler. "On typical embedded processors, code generated by CompCert typi­cally runs twice as fast as code generated by GCC without optimizations, and only 20% slower than GCC code at optimization level 3. Details about the benchmark mix used to obtain these numbers are avail­able on request."

CompCert is free for non-commercial use.

Retrieved from "https://simson.net/wiki/index.php?title=Formal_Verification&oldid=1673"