09:00‑10:00 SAT SMT Tutorial
Location: IF G.07A
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 |