DATALOG_SOLVE: A Datalog-Based Demand-Driven Program Analyzer

详细信息    查看全文

• 作者：M. Alpuente ; M.A. Feliú ; C. Joubert ; A. Villanueva
• 关键词：Java program analysis ; Datalog ; boolean equation system ; demand-driven evaluation
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2009
• 出版时间：5 August 2009
• 年：2009
• 卷：248
• 期：Complete
• 页码：57-66
• 全文大小：257 K

文摘

This work presents a practical Java program analysis framework that is obtained by combining a Java virtual machine with a general-purpose verification toolbox that we previously extended. In our methodology, Datalog clauses are used to specify complex interprocedural program analyses involving dynamically created objects. After extracting an initial set of Datalog constraints about the Java bytecode program semantics, our framework transforms the Datalog rules of a particular analysis into a Boolean Equation System (value=""smcaps"">Bes), whose local resolution using the aforementioned extended verification toolbox corresponds to the demand-driven computation of the analysis.