|
|
|
|
|
|
by syrak
1876 days ago
|
|
|
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. |
|
|