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 |