Guest Speaker: Grigory Fedyukovich, Assistant Professor, Florida State University, and Visiting Academic at Amazon
Date: Thursday, June 15, 2023
Time: 1:00pm
Location: E5 4047
Hosted
by:
Professor
Arie
Gurfinkel
Abstract:
State-of-the-art
solvers
for
constrained
Horn
clauses
(CHC)
are
successfully
used
to
generate
reachability
facts
from
symbolic
encodings
of
programs.
In
this
talk,
I
will
present
a
new
application
of
CHCs
to
test-case
generation,
a
problem
of
finding
a
set
of
tuples
of
input
values
to
a
program
under
which
the
program
visits
as
many
branches
as
possible.
However,
if
a
block
of
code
is
provably
unreachable,
no
test
case
can
be
generated
allowing
to
explore
other
blocks
of
code.
Our
new
approach
uses
CHC
to
incrementally
construct
different
program
unrollings
and
extract
test
cases
from
models
of
satisfiable
formulas.
At
the
same
time,
a
CHC
solver
keeps
track
of
CHCs
that
represent
unreachable
blocks
of
code
which
makes
the
unrolling
process
more
efficient.
In
practice,
this
lets
our
approach
to
terminate
early
while
guaranteeing
maximal
coverage.
Our
implementation
called
HORNTINUUM
exhibits
promising
performance:
it
generates
high
coverage
in
the
majority
of
cases
and
spends
less
time
on
average
than
state-of-the-art
based
on
bounded
model
checking,
concolic
execution,
and/or
fuzzing.
Biography:
Grigory
Fedyukovich
is
an
Assistant
Professor
at
Florida
State
University
and
a
Visiting
Academic
at
Amazon.
He
completed
his
Ph.D.
at
the
University
of
Lugano
under
the
supervision
of
Prof
Natasha
Sharygina
and
then
a
postdoc
at
the
University
of
Washington
with
Prof
Rastislav
Bodik
and
at
Princeton
University
with
Prof
Aarti
Gupta.
His
main
research
interests
are
in
the
fields
of
automated
reasoning,
software
verification,
and
synthesis.