Difference between revisions of "Formal Verification"

From Simson Garfinkel
Jump to navigationJump to search
(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...")
 
m (Redirected page to Secure coding tools)
Tag: New redirect
 
Line 1: Line 1:
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."
#REDIRECT [[Secure coding tools]]
 
CompCert is free for non-commercial use.
 
* [http://compcert.inria.fr Project page]
* [https://en.wikipedia.org/wiki/CompCert Wikipedia article on CompCert]
* [https://github.com/AbsInt/CompCert Github Repository]
* [https://www.absint.com/compcert/ Comparision with GCC]

Latest revision as of 04:12, 27 June 2018

Redirect to:

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