3 ms·

I believe they're also used for verifying potential new compiler optimizations: http://blog.regehr.org/archives/247 http://blog.regehr.org/archives/247 Check o

by mayank 16y ago

I believe they're also used for verifying potential new compiler optimizations: http://blog.regehr.org/archives/247 http://blog.regehr.org/archives/247 Check out the SAT competition for state of the art solvers: http://www.satcompetition.org/ http://www.satcompetition.org/

jules 16y ago
They can also be used to do the actual optimizations. For example most formulations of the register allocation problem are NP-complete. SMT formulas can be used as a very powerful abstract domain in abstract interpretation.