...
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
...
...
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 |
|---|
...
|
...
|
...