SMT on Wednesday, July 14th

10:30‑11:30 Invited Talk
Location: IF G.07A
10:30 Nikolai Tillman, Microsoft
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.

11:30‑12:30 Session 1
Location: IF G.07A
11:30 B. Paleo, S. Merz, P. Fontaine
Exploring and Exploiting Algebraic and Graphical Properties of Resolution
12:00 M. Bankovic and F. Maric
Alldifferent Constraint Solver in SMT
14:00‑14:50 Joint SAT/SMT Session
Location: AT LT2
14:00 Miquel Bofill, Josep Suy and Mateu Villaret
(SAT'10) A system for solving constraint satisfaction problems with SMT
14:20 J. Christ, J. Hoenicke
Instantiation-Based Interpolation for Quantified Formulae
15:30‑16:00 Session 2
Location: IF G.07A
15:30 C. Barrett, A. Stump, C. Tinelli
The SMT-LIB Standard – Version 2.0