...
UCLID's
...
Elements:
...
Term-Level
...
Verification
...
and
...
SMT
...
Solving
...
UCLID
...
is
...
a
...
toolkit
...
for
...
modeling
...
and
...
verifying
...
systems,
...
both
...
finite
...
-
...
and
...
infinite-state,
...
at
...
the
...
term
...
level
...
.
...
The
...
phrase
...
"term
...
level"
...
refers
...
to
...
the
...
use
...
of
...
first-order
...
logic
...
with
...
background
...
theories
...
in
...
modeling
...
and
...
verification.
...
This
...
talk
...
will
...
describe
...
the
...
key
...
elements
...
of
...
UCLID:
...
(i)
...
term-level
...
abstraction
...
-
...
-
...
the
...
process
...
of
...
creating
...
term-level
...
models
...
from
...
implementations;
...
(ii)
...
term-level
...
verification
...
-
...
-
...
the
...
verification
...
strategies
...
available
...
in
...
UCLID,
...
and
...
(iii)
...
SMT
...
solving
...
-
...
-
...
the
...
decision
...
procedures
...
within
...
UCLID
...
that
...
form
...
its
...
computational
...
engine.
...
UCLID
...
has
...
been
...
applied
...
to
...
several
...
application
...
areas,
...
including
...
hardware
...
verification
...
and
...
synthesis,
...
computer
...
security,
...
software
...
analysis,
...
and
...
hybrid
...
systems
...
verification
...
--
...
-
...
this
...
talk
...
will
...
touch
...
upon
...
some
...
of
...
these
...
applications.
...
Talk
...
slides
...
available
...
...
...
...
.
Randy Bryant & Sanjit Seshia, CMU, Pittsburgh and UC, Berkeley, USA
Click here for biographies: Randy Bryant, Sanjit Seshia
| Attachments | ||
|---|---|---|
|