Hacker News
new
|
past
|
comments
|
ask
|
show
|
jobs
|
submit
login
regehr
on June 24, 2014
|
parent
|
context
|
favorite
| on:
Sel4: We’re going open source
John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.
chubot
on June 24, 2014
|
next
[–]
Sounds interesting -- is there a paper that describes this?
regehr
on June 24, 2014
|
parent
|
next
[–]
I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here:
http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf
wglb
on June 24, 2014
|
prev
[–]
My error.
Guidelines
|
FAQ
|
Lists
|
API
|
Security
|
Legal
|
Apply to YC
|
Contact
Search:
