2 ms·
Don't SMT solvers output proof objects so that the results can be easily independently verified?
by creata 5y ago
Don't SMT solvers output proof objects so that the results can be easily independently verified?
- syrak 5y agoEven 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.