...
SAT
...
Solvers
...
for
...
Formal
...
Verification
...
put
...
your
...
abstract
...
here
Ed Clarke, Carnegie Mellon University, Pittsburgh, USA
Edmund M. Clarke received a B.A.
...
degree
...
in
...
mathematics
...
from
...
the
...
University
...
of
...
Virginia,
...
Charlottesville,
...
VA,
...
in
...
1967,
...
an
...
M.A.
...
degree
...
in
...
mathematics
...
from
...
Duke
...
University,
...
Durham
...
NC,
...
in
...
1968,
...
and
...
a
...
Ph.D.
...
degree
...
in
...
Computer
...
Science
...
from
...
Cornell
...
University,
...
Ithaca
...
NY,
...
in
...
1976.
...
After
...
receiving
...
his
...
Ph.D.,
...
he
...
taught
...
in
...
the
...
Department
...
of
...
Computer
...
Science,
...
Duke
...
University,
...
for
...
two
...
years.
...
In
...
1978
...
he
...
moved
...
to
...
Harvard
...
University,
...
Cambridge,
...
MA
...
where
...
he
...
was
...
an
...
Assistant
...
Professor
...
of
...
Computer
...
Science
...
in
...
the
...
Division
...
of
...
Applied
...
Sciences.
...
He
...
left
...
Harvard
...
in
...
1982
...
to
...
join
...
the
...
faculty
...
in
...
the
...
Computer
...
Science
...
Department
...
at
...
Carnegie-Mellon
...
University,
...
Pittsburgh,
...
PA.
...
He
...
was
...
appointed
...
Full
...
Professor
...
in
...
1989.
...
In
...
1995
...
he
...
became
...
the
...
first
...
recipient
...
of
...
the
...
FORE
...
Systems
...
Professorship,
...
an
...
endowed
...
chair
...
in
...
the
...
School
...
of
...
Computer
...
Science.
...
He
...
was
...
named
...
a
...
University
...
Professor
...
in
...
2008
...
Dr.
...
Clarke's
...
interests
...
include
...
software
...
and
...
hardware
...
verification
...
and
...
automatic
...
theorem
...
proving.
...
In
...
his
...
Ph.D.
...
thesis
...
he
...
proved
...
that
...
certain
...
programming
...
language
...
control
...
structures
...
did
...
not
...
have
...
good
...
Hoare
...
style
...
proof
...
systems.
...
In
...
1981
...
he
...
and
...
his
...
Ph.D.
...
student
...
Allen
...
Emerson
...
first
...
proposed
...
the
...
use
...
of
...
Model
...
Checking
...
as
...
a
...
verification
...
technique
...
for
...
finite
...
state
...
concurrent
...
systems.
...
His
...
research
...
group
...
pioneered
...
the
...
use
...
of
...
Model
...
Checking
...
for
...
hardware
...
verification.
...
Symbolic
...
Model
...
Checking
...
using
...
BDDs
...
was
...
also
...
developed
...
by
...
his
...
group.
...
This
...
important
...
technique
...
was
...
the
...
subject
...
of
...
Kenneth
...
McMillan's
...
Ph.D.
...
thesis,
...
which
...
received
...
an
...
ACM
...
Doctoral
...
Dissertation
...
Award.
...
In
...
addition,
...
his
...
resarch
...
group
...
developed
...
the
...
first
...
parallel
...
resolution
...
theorem
...
prover
...
(Parthenon)
...
and
...
the
...
first
...
theorem
...
prover
...
to
...
be
...
based
...
on
...
a
...
symbolic
...
computation
...
system
...
(Analytica).
...
Dr.
...
Clarke
...
has
...
served
...
on
...
the
...
editorial
...
boards
...
of
...
Distributed
...
Computing,
...
Logic
...
and
...
Computation,
...
and
...
IEEE
...
Transactions
...
in
...
Software
...
Engineering.
...
He
...
is
...
the
...
former
...
editor-in-chief
...
of
...
Formal
...
Methods
...
in
...
Systems
...
Design.
...
He
...
is
...
on
...
the
...
organizing
...
committee
...
of
...
Logic
...
in
...
Computer
...
Science
...
(LICS)
...
and
...
on
...
the
...
steering
...
committee
...
of
...
Computer-Aided
...
Verification
...
(CAV).
...
He
...
received
...
a
...
Technical
...
Excellence
...
Award
...
with
...
Randy
...
Bryant
...
and
...
Ken
...
McMillan
...
from
...
the
...
Semiconductor
...
Research
...
Corporation
...
in
...
1995
...
for
...
his
...
work
...
on
...
formal
...
verification
...
techniques.
...
He
...
was
...
a
...
co-winner
...
with
...
Randy
...
Bryant,
...
Allen
...
Emerson,
...
and
...
Kenneth
...
McMillan
...
of
...
the
...
ACM
...
Kanellakis
...
Award
...
in
...
1998
...
for
...
the
...
development
...
of
...
Symbolic
...
Model
...
Checking.
...
In
...
1999
...
he
...
received
...
an
...
Allen
...
Newell
...
Award
...
for
...
Excellence
...
in
...
Research
...
from
...
the
...
Carnegie
...
Mellon
...
Computer
...
Science
...
Department.
...
In
...
2004
...
he
...
received
...
the
...
IEEE
...
Harry
...
H.
...
Goode
...
Memorial
...
Award
...
for
...
significant
...
and
...
pioneering
...
contributions
...
to
...
formal
...
verification
...
of
...
hardware
...
and
...
software
...
systems,
...
and
...
for
...
the
...
profound
...
impact
...
these
...
contributions
...
have
...
had
...
on
...
the
...
electronics
...
industry.
...
He
...
was
...
elected
...
to
...
the
...
National
...
Academy
...
of
...
Engineering
...
in
...
2005
...
for
...
contributions
...
to
...
the
...
formal
...
verification
...
of
...
hardware
...
and
...
software
...
correctness.
...
He
...
was
...
a
...
recipient
...
with
...
Allen
...
Emerson
...
and
...
Joseph
...
Sifakis
...
of
...
the
...
2007
...
ACM
...
Turing
...
Award
...
for
...
his
...
role
...
in
...
developing
...
Model
...
Checking
...
into
...
a
...
highly
...
effective
...
verification
...
technology,
...
widely
...
adopted
...
in
...
the
...
hardware
...
and
...
software
...
industries.
...
In
...
2008
...
he
...
received
...
the
...
CADE
...
Herbrand
...
Award
...
for
...
Distinguished
...
Contributions
...
to
...
Automated
...
Reasoning
...
in
...
recognition
...
of
...
his
...
role
...
in
...
the
...
invention
...
of
...
Model
...
Checking
...
and
...
his
...
sustained
...
leadership
...
in
...
the
...
area
...
for
...
more
...
than
...
two
...
decades.
...
In
...
2011
...
he
...
was
...
elected
...
to
...
the
...
American
...
Academy
...
of
...
Arts
...
&
...
Sciences
...
which
...
includes
...
distinguished
...
leaders
...
in
...
the
...
sciences,
...
social
...
sciences,
...
the
...
humanities,
...
the
...
arts,
...
as
...
well
...
as
...
business
...
and
...
public
...
affairs.
...
Dr.
...
Clarke
...
is
...
a
...
Fellow
...
of
...
the
...
ACM
...
and
...
the
...
IEEE,
...
and
...
a
...
member
...
of
...
Sigma
...
Xi
...
and
...
Phi
...
Beta
...
Kappa.
...
| Attachments | ||
|---|---|---|
|
...