...
OpenSMT
...
and
...
Applications:
...
Lazy
...
Abstraction,
...
Interpolants,
...
Proof
...
Reduction
...
We
...
describe
...
OpenSMT
...
and
...
show
...
its
...
use
...
(with
...
demos)
...
when
...
applied
...
to
...
the
...
Lazy-abstraction
...
(with
...
interpolants)
...
framework,
...
interpolants
...
computation,
...
interpolants
...
strenght,
...
and
...
unsatisfiability-proof
...
reduction.
...
Roberto Bruttomesso & Natasha Sharygina, University of Lugano, Lugano, Switzerland
Roberto received a M.S.
...
Degree
...
from
...
the
...
University
...
of
...
Milan
...
(advisor
...
S.
...
Ghilardi),
...
in
...
2004,
...
and
...
a
...
Doctoral
...
Degree
...
from
...
the
...
University
...
of
...
Trento
...
(advisor
...
A.
...
Cimatti),
...
in
...
2008.
...
Currently
...
he
...
is
...
a
...
Post-Doc
...
in
...
the
...
Formal
...
Verification
...
Group
...
at
...
the
...
University
...
of
...
Lugano.
...
His
...
main
...
research
...
interests
...
include
...
decision
...
procedures
...
and
...
in
...
particular
...
satisfiability
...
modulo
...
theories
...
applied
...
to
...
model
...
checking
...
for
...
the
...
verification
...
of
...
hardware
...
and
...
software.
...
----------------------------------------------------------------------------
...
-
...
Natasha
...
Sharygina
...
is
...
a
...
Professor
...
of
...
Informatics
...
at
...
the
...
University
...
of
...
Lugano,
...
Switzerland
...
and
...
an
...
adjunct
...
Professor
...
at
...
School
...
of
...
Computer
...
Science,
...
Carnegie
...
Mellon
...
University,
...
Pittsburgh,
...
USA.
...
Prof.
...
Sharygina
...
received
...
a
...
Ph.D.
...
degree
...
from
...
the
...
University
...
of
...
Texas
...
at
...
Austin,
...
USA
...
in
...
2002.
...
Her
...
professional
...
experience
...
includes
...
consulting
...
at
...
Bell
...
Labs,
...
Lucent
...
Technologies
...
at
...
the
...
Computing
...
Sciences
...
Research
...
in
...
2000-2001
...
and
...
a
...
research
...
faculty
...
position
...
at
...
Carnegie
...
Mellon
...
University,
...
SEI
...
in
...
2002-2005.
...
Prof.
...
Sharygina
...
directs
...
the
...
...
...
...
...
...
group whose research deals with improving the program development process through formal methods of specification and verification. Prof. Sharygina’s research has been funded by multiple grants including the CMU SEI Independent R&D grants, Tasso Career, the Swiss National Foundation, and European Union Research grants. Prof. Sharygina has authored more than 55 research papers in areas of formal verification, and system design. She served on program committees of various conferences (e.g.,
...
TACAS,
...
FMCAD,
...
CAV),
...
given
...
keynote
...
and
...
invited
...
presentations,
...
and
...
co-chaired
...
several
...
workshops
...
in
...
the
...
area
...
of
...
formal
...
verification.
...
Prof.
...
Sharygina
...
is
...
chairing
...
FMCAD
...
2010
...
and
...
CAV
...
2013,
...
the
...
major
...
conferences
...
in
...
computer-aided
...
verification
...
and
...
design.
...
| Attachments |
|---|
...
|
...
|
...