Revamping TVLA: Making Parametric Shape Analysis Competitive
Revamping TVLA: Making Parametric Shape Analysis Competitive
复制标题
改进 TVLA：使参数形状分析具有竞争力
DOI：
10.1007/978-3-540-73368-3_25
复制
发表时间：
2007
影响因子：
3.3
通讯作者：
Shmuel Sagiv
中科院分区：
文献类型：
--
作者：
Igor Bogudlov;T. Lev;T. Reps;Shmuel Sagiv
TVLA是用于形状分析的参数框架，可以很容易地实例化以创建不同种类的分析仪，以检查使用链接数据结构的程序的属性。我们报告了TVLA性能的显着改善，这使参数形状分析的成本与最有效的专业形状 - 分析工具（限制了所分析的数据结构和程序类别）相当，而无需牺牲TVLA的参数性。这些改进是通过采用来自数据库社区的知名技术来降低从形状描述符中提取信息的成本并对程序声明和条件进行抽象解释来获得的。与先前版本的TVLA相比，我们获得了多达50倍的速度。
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.