...
HAMPI:
...
A
...
Solver
...
for
...
String
...
Theories
...
Strings
...
are
...
used
...
everywhere
...
from
...
Web
...
apps
...
written
...
in
...
PHP/JavaScript
...
to
...
programs
...
written
...
in
...
Java/C/C++.
...
Analysis
...
of
...
such
...
programs
...
usually
...
results
...
in
...
string
...
constraints,
...
i.e.,
...
formulas
...
that
...
are
...
constructed
...
out
...
of
...
string
...
variables,
...
constants,
...
concat,
...
extract
...
and
...
string
...
comparison.
...
In
...
addition,
...
many
...
of
...
these
...
programs
...
have
...
sanitization
...
code
...
that
...
are
...
constructed
...
out
...
of
...
regular
...
expressions
...
and
...
context-free
...
grammars.
...
In
...
order
...
to
...
support
...
the
...
analysis
...
of
...
string-manipulating
...
programs
...
we
...
wrote
...
HAMPI,
...
a
...
solver
...
for
...
string
...
constraints.
...
HAMPI
...
has
...
been
...
used
...
in
...
more
...
than
...
a
...
dozen
...
projects
...
from
...
static
...
to
...
dynamic
...
analysis,
...
from
...
testing
...
to
...
vulnerability
...
detection.
...
In
...
this
...
talk,
...
I
...
will
...
introduce
...
a
...
theory
...
of
...
strings
...
supported
...
by
...
HAMPI,
...
examples
...
of
...
how
...
HAMPI
...
can
...
be
...
used,
...
and
...
I
...
will
...
explain
...
how
...
HAMPI
...
works.
...
Vijay Ganesh, MIT, Cambridge, USA
Dr. Vijay Ganesh is a Research Scientist at MIT since October 2007, and he will join IMDEA as an assistant professor in late 2011/early 2012. He completed his PhD in computer science from Stanford University in September 2007. He also has two MS degrees in computer science and electrical engineering, both from Stanford University, and Bachelor of Technology degree from College of Engineering, Trivandrum, India.
His primary research interests are constraint solvers (SAT/SMT solvers), and their applications to software reliability, computer security and biology. He works on both the theory and practice of constraint solvers. He has designed and implemented several constraint solvers, most notably, STP and HAMPI. STP was one of the first solvers to enable an exciting new testing technique called systematic dynamic testing (or concolic testing). STP has been used in more than 100 research projects relating to software reliability and computer security. More recently he designed another solver, HAMPI, aimed at solving string constraints generated by the analysis of PHP, JavaScript and Perl programs. His paper on HAMPI won the ACM Distinguished Paper Award (2009). STP was the co-winner of the SMTCOMP competition for bit-vector solvers in 2006, and the winner in 2010. Dr. Ganesh has also done research in automated software testing, in particular, whitebox fuzzing, and hardware archictecture description languages.
Besides his primary research interest, Dr. Ganesh is also interested in self-adaptive software (self-* programming), i.e., software that adapts itself to the environment. His other interests include quantum information theory and quantum computing.
| Attachments | ||
|---|---|---|
|