Revamping TVLA: Making Parametric Shape Analysis Competitive
Igor Bogudlov, Tal Lev-Ami, Thomas Reps, and Mooly Sagiv
TVLA is a parametric framework for shape analysis that can be easily
instantiated to create different kinds of analyzers for checking
properties of programs that use linked data structures.
We report on dramatic improvements in TVLA's performance,
which make the cost of parametric shape analysis comparable to that of the
most efficient specialized shape-analysis tools (which restrict
the class of data structures and programs analyzed)
without sacrificing TVLA's parametricity.
The improvements were obtained by employing well-known techniques from
the database community to reduce the cost of extracting information
from shape descriptors and performing abstract interpretation of
program statements and conditions.
Compared to the prior version of TVLA, we obtained as much as
50-fold speedup.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)