4 ms·
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.
by regehr 12y ago
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.
- wglb 12y agoMy error.
- chubot 12y agoSounds interesting -- is there a paper that describes this?
- regehr 12y agoI 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 http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf