SMT on Thursday, July 15th

09:00‑10:00 Invited Talk
Location: IF G.07A
09:00 Silvio Ghilardi, U. Milano
SMT model checking for array-based systems

We show how to exploit SMT solvers in declarative formulations of classical backward reachability algorithms. We motivate the notion of an array-based system and introduce some decision problems for quantified formulae arising from infinite state model checking applications. We also show how this framework is implemented in the model checker MCMT (based on the SMT solver Yices). Finally we discuss some common benchmarks in the area of distributed algorithms and report also recent experiments concerning timed and fault tolerant systems. We shall discuss the efficiency of strategies for invariant synthesis and for partially interactive verification in our experiments.

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