This approach is interesting, it's also used by compcert for its register allocator; the allocator itself is not formally verified, but the its results are. It's not complete, in a general sense, but I wonder if this sort of 'brute-force' approach to formal verification will become more popular over time, and lower the barrier to entry for formally verifying nontrivial programs.
> In CompCert's case though, the register allocation verifier itself is verified.
I don't think so, I think moonchild's account of it is accurate. At least, it was accurate in 2012. From a 2012 blog post: [0]
> In CompCert, this algorithm is not proven correct. Instead, after generating the graph, the compiler calls an OCaml implementation of IRC and then checks that the coloring is valid. If the checker confirms that the coloring is valid, the compiler uses it and proceeds along. If it does not confirm that it's valid, compilation is aborted. This checker is proven correct, and because it is simpler, its proof of correctness is easier.
> This checker is proven correct, and because it is simpler, its proof of correctness is easier.
Still correct ;)
What I belief GP (fuklief) meant was: The SMT solver might still be incorrect. Like the register allocator itself in CompCert. But for CompCert, the result is checked by a formally verified checker. I do not know if that's true or not for the result of the SMT solver.
Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.
