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

.

h1. [Bruno Dutertre|http://www.csl.sri.com/people/bruno/], 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.

{attachments

:patterns

=.*}