Program of SMT

Wednesday, July 14th

Wednesday's program is also available with abstracts and side by side with other events.

10:30‑11:30 Invited Talk
Location: IF G.07A
10:30 Nikolai Tillman, Microsoft
SMT-Solvers In (Tracing) Just-in-Time Compilers
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
Thursday, July 15th

Thursday's program is also available with abstracts and side by side with other events.

09:00‑10:00 Invited Talk
Location: IF G.07A
09:00 Silvio Ghilardi, U. Milano
SMT model checking for array-based systems
10:30‑12:30 Session 3
Location: IF G.07A
10:30 M. Ganai, F. Ivancic
Efficient Decision Procedure for Non-linear Arithmetic Constraints using CORDIC
11:00 E. Abraham, U. Loup, F. Corzilius, T. Sturm
A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra
11:30 Frederic Besson
On using an inexact floating-point LP solver for deciding linear arithmetic in a SMT solver
12:00 P. Rümmer and T. Wahl
An SMT-LIB Theory of Binary Floating-Point Arithmetic
14:00‑15:00 Session 4
Location: IF G.07A
14:00 D. Jovanovic and C. Barrett
Sharing is Caring
14:30 L. Cordeiro, B Fischer
Bounded Model Checking of Multi-threaded Software using SMT solvers
15:30‑17:00 Session 5
Location: IF G.07A
15:30 A. Griggio
A Practical Approach to SMT(LA(Z))
16:00 A. Reynolds, L. Hadarean, C. Tinelli, Y. Ge, A. Stump, C. Barrett
Comparing Proof Systems for Linear Real Arithmetic with LFSC
16:30 A report on the SMT Competition