Sub-Computation Based Transition Predicate Abstraction

• Item type: Trans(1)
• 公開日: 2007-06-15
• タイトル: Sub-Computation Based Transition Predicate Abstraction
• タイトル / 言語: en
• タイトル: Sub-Computation Based Transition Predicate Abstraction
• 言語: eng
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: Department of Computer Science Graduate School of Information Science and Technology the University of Tokyo
• 著者所属: Department of Computer Science Graduate School of Information Science and Technology the University of Tokyo
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo
• 著者名: CarlChristianFrederiksen; Masami, Hagiya
• 著者名(英): Carl, ChristianFrederiksen; Masami, Hagiya
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: The transition predicate abstraction framework developed by Podelski et al. (2005) captures size relations over state transitions which can be used to show infeasibility of certain program computations. In particular general liveness properties (i.e. properties of infinite computations) can be verified by reducing the verification problem to one of fair termination and then proving that all (infinite) fair computations are infeasible. We present an extension of the algorithm by Podelski et al. that can be used to improve the precision of transition predicate abstraction as well as speed up analysis time for programs with well-structured control-flow. The main key is to identify sub-computations that can be evaluated independently of their context. Efficiency is then readily improved by analyzing each sub-computation in turn thus avoiding to reanalyze the effect of a given sub-computations for different contexts. Further precision can be improved by using stronger methods for extracting summary information about a given sub-computation. We present two versions of the sub-computation based analysis: one for a non-parallel imperative language with loops and recursive procedures serving as an introduction and one for the extension of the non-parallel language to a parallel language with synchronous communication via statically named channels.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: The transition predicate abstraction framework developed by Podelski, et al. (2005) captures size relations over state transitions which can be used to show infeasibility of certain program computations. In particular, general liveness properties (i.e., properties of infinite computations) can be verified by reducing the verification problem to one of fair termination and then proving that all (infinite) fair computations are infeasible. We present an extension of the algorithm by Podelski, et al. that can be used to improve the precision of transition predicate abstraction as well as speed up analysis time for programs with well-structured control-flow. The main key is to identify sub-computations that can be evaluated independently of their context. Efficiency is then readily improved by analyzing each sub-computation in turn, thus avoiding to reanalyze the effect of a given sub-computations for different contexts. Further, precision can be improved by using stronger methods for extracting summary information about a given sub-computation. We present two versions of the sub-computation based analysis: one for a non-parallel imperative language with loops and recursive procedures, serving as an introduction, and one for the extension of the non-parallel language to a parallel language with synchronous communication via statically named channels.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 48, 号 SIG10(PRO33), p. 114-137, 発行日 2007-06-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会