Sub-Computation Based Transition Predicate Abstraction

• Frederiksen Carl Christian

  Department of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo

• Hagiya Masami

  Department of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo

抄録

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.

収録刊行物

• Information and Media Technologies

  Information and Media Technologies 2 (3), 773-796, 2007

  Information and Media Technologies 編集運営会議

詳細情報

• CRID: 1390001205264870144
• NII論文ID: 130000058271
• DOI: 10.11185/imt.2.773
• ISSN: 18810896
• 本文言語コード: en
• データソース種別:
  • JaLC
  • CiNii Articles
• 抄録ライセンスフラグ: 使用不可