Yices and Applications

Yices is an efficient SMT solver developed by SRI International. It supports theories such as uninterpreted functions, linear arithmetic,
extensional arrays, and bit-vectors, which have many practical applications. The talk will give an overview of Yices features and
architecture, and present two representative examples of applications. The first example is the computation of communication
schedules for the Timed-Triggered Ethernet. The second example describes an application of SMT solvers to the verification of
real-time systems, using techniques related to bounded model checking and k-induction.

Bruno Dutertre, SRI International, Menlo Park, USA

Bruno Dutertre is a Senior Computer Scientist in the Computer Science Laboratory of SRI International. His main research interests include
decision procedures, SMT solving, and the application of logic, theorem proving and model checking to the engineering of
high-integrity systems. He is developer and maintainer of Yices, SRI's state-of-the-art SMT solver, which is freely available at http://yices.csl.sri.com/. He also contributes to the development of SRI's Symbolic Analysis Laboratory (SAL) a toolset for
modeling and model checking of state-transition systems.