The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Sorry, I have to fix one thing.

Actually what we did is not a strong induction.

We might be able to call it a strong coinduction.

We will introduce the idea in a future paper.

Best,

Gil

On Sun, Jan 11, 2015 at 12:26 AM, Chung-Kil Hur <gil.hur AT gmail.com> wrote:

Dear Coq-Club,

We are happy to announce that we completed the correctness proof of
separate compilation of CompCert 2.4. Our proof is essentially based
on a strong induction.

Our proof is an add-on package for CompCert 2.4 and the whole
development is about 6K LOC and took one person-month.

You can find the details at

http://sf.snu.ac.kr/compcertsep .

During the proof, we found two bugs in CompCert 2.4. One is due to an
invalid axiom assumed and the other is due to an analysis that is
invalidated in the presence of linking. We think this shows why we
should verify separate compilation though linking seems so simple.  In
general, we learned a lesson that we cannot trust any simple property
unless verified or very carefully examined.

These bugs are reported to Xavier Leroy and the second bug is fixed in
the CompCert repository. We are currently waiting for the first bug to
be fixed. Our add-on package contains the fix for the second bug and
assumes some axiom that is not true at the moment but should be true
after the first bug is fixed.

You can find the counter examples showing the bugs in the above web page.

Best regards,
Jeehoon Kang and Chung-Kil Hur,
Seoul National University