4 ms·

http://compcert.inria.fr/ http://compcert.inria.fr/ CompCert is a verified compiler that transforms code from "virtual machine" of language C to "virtual machi

by thesz 15y ago

http://compcert.inria.fr/ http://compcert.inria.fr/ CompCert is a verified compiler that transforms code from "virtual machine" of language C to "virtual machine" of PowerPC. It is generated from Coq, though. But, please see ynot: http://ynot.cs.harvard.edu/ http://ynot.cs.harvard.edu/ They have a verified SQL compiler. Again, generated from Coq source. So I think you're wrong claiming that static analysis isn't useful for virtual machines. For C you have to have very extensive annotations, as it is not very expressive by itself, but static analysis is still possible.

_delirium 15y ago
That's true, but I think a different class of tools: theorem-provers that depend on extensive domain-specific annotations (e.g. about SQL semantics) to prove correctness aren't usually applied in the same situations as tools like Coverity that do static analysis of raw C/C++ code to find likely bugs; though there's some convergence in the past 10 years.