Revamping TVLA: Making Parametric Shape Analysis Competitive

Abstract. 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.

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv
• Keywords: CAV 2007, Data Structures, Formal Methods, Parametric Shape Analysis, Shape Analysis