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. © Springer-Verlag Berlin Heidelberg 2007.
Mendeley helps you to discover research relevant for your work.
CITATION STYLE
Bogudlov, I., Lev-Ami, T., Reps, T., & Sagiv, M. (2007). Revamping TVLA: Making parametric shape analysis competitive. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4590 LNCS, pp. 221–225). Springer Verlag. https://doi.org/10.1007/978-3-540-73368-3_25