[marco2357]

Only in the form of translating and running dozens of C applications (programs and libraries) and running their testsuites. E.g. libcurl comes with a great extensive testsuite (a perl script running against the binary).

Translated applications still need to be thoroughly tested and usually some bugs are still found.

So we didn't formalize and verify our translation. Interestingly enough, we run into bugs in javac and ecj (Eclipse Java Compiler) surprisingly often. So verifying our translation would still lead to translations with bugs ;-)

Another fun fact: Since our translation knows the limits of allocated memory (and many other things), we found many illegal memory accesses in C programs that were unknown before (libgmp, micro httpd, vim, ...) since they didn't (or only very seldomly) lead to segfaults.

[danieltillett]

This sounds like a great spin off - bug finding in C code. Have you put much thought into pursuing this?

[marco2357]

Didn't think too much about it since there are many C specific analyzers and tools that do the same. Well, they do it way better. E.g. Valgrind.

[danieltillett]

I would guess the value would be if you find bugs that other tools don't. If you just find the same bugs as Valgrind then I agree that there would not be too much value, but if you find unique bugs then it would be useful.