...
CVC3
...
and
...
Applications
...
The
...
first
...
part
...
of
...
this
...
talk
...
covers
...
the
...
history
...
and
...
progression
...
of
...
SMT
...
solvers
...
I
...
have
...
worked
...
on,
...
starting
...
with
...
SVC,
...
and
...
then
...
continuing
...
with
...
CVC,
...
CVC
...
Lite,
...
CVC3,
...
and
...
finally
...
CVC4,
...
describing
...
innovations,
...
applications,
...
limitations,
...
and
...
lessons
...
learned
...
along
...
the
...
way.
...
The
...
second
...
part
...
of
...
the
...
talk
...
describes
...
a
...
specific
...
application
...
of
...
CVC3
...
to
...
verify
...
low-level
...
packet
...
processing
...
code
...
in
...
C.
...
This
...
application
...
makes
...
use
...
of
...
a
...
large
...
number
...
of
...
features
...
including
...
uninterpreted
...
functions,
...
data
...
types,
...
bit-vectors,
...
arrays,
...
and
...
quantifiers.
...
Clark Barrett, New York University, New York, USA
Clark Barrett received his bachelor's degree in Mathematics, Computer Science, and Electrical Engineering from Brigham Young University in 1995. He received his PhD from Stanford University and joined the faculty of New York University in the Fall of 2002.
His industry experience includes work on formal hardware verification at Intel's Strategic CAD Labs, as well as work on formal and semi-formal hardware verification tools at 0-in Design Automation (now part of Mentor Graphics).
Professor Barrett's research agenda includes the theory, implementation, and application of advanced automated deduction and theorem proving. His SMT tools have been widely used. He received an IBM Software Quality Innovation Award for CVC3 in November 2008 and the 2010 HVC award (with Leonardo de Moura, Silvio Ranise, Aaron Stump, and Cesare Tinelli) for his work helping to establish and support the SMT community.
| Attachments | ||
|---|---|---|
|