Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
primodemus
on Jan 12, 2011
|
parent
|
context
|
favorite
| on:
The PHP strtod() denial of service bug
He also points to Compcert: a certified compiler for a subset of C. The compiler is specified, programmed and proved in Coq. It is a really impressive project:
http://compcert.inria.fr/compcert-C.html
rwmj
on Jan 12, 2011
[–]
Compcert is great (it's by the same team who do OCaml). Unfortunately however it's not free software.
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search: