ABOUT FLOC
HOME About FLoC Sponsors Mailing list Contact
PARTICIPATION
Registration Accommodation Student travel support US-based Student travel support Visa information Cancellation Policy Local information Reimbursement forms (new!)
MEETINGS
CAV CSF ICLP IJCAR ITP LICS RTA SAT Workshops (alpha.) Workshops (by conf.) Affiliated Events
PROGRAM
FLoC at a glance Meeting by meeting Day by day Room assignment Invited talks Accepted papers Social events FLoC Brochure (PDF)
!! LAST MINUTE NEWS !! !! ROOM CHANGES !!
ORGANIZATION
Steering Committee Programme Committee Organising Committee
MISCELLANEOUS
Call for Workshops

Program of SMT

Wednesday, July 14th

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

09:00‑10:00 SAT SMT Tutorial
Location: IF G.07A
10:00‑10:30 Coffee break
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
12:30‑14:00 Lunch
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:00‑15:30 Coffee break
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:00‑10:30 Coffee break
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
12:30‑14:00 Lunch
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:00‑15:30 Coffee break
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