4 ms·
> 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 SM
by archi42 5y ago
> 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.
- creata 5y agoDon'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.