Nikolai Tillmann, Microsoft Research
SMT-Solvers In (Tracing) Just-in-Time Compilers

Tracing just-in-time compilers determine frequently executed traces (hot paths and loops) at run time. These traces are then analyzed and optimized, and finally specialized machine code is generated. Up to now, tracing just-in-time compilers employed standard compiler construction algorithms to analyze and optimize traces. We propose to leverage SMT solvers to optimize traces at run time.