{"links":{},"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00016507","sets":["934:935:945:947"]},"path":["947"],"owner":"1","recid":"16507","title":["Sub-Computation Based Transition Predicate Abstraction"],"pubdate":{"attribute_name":"公開日","attribute_value":"2007-06-15"},"_buckets":{"deposit":"6695bc2b-d824-4e99-ac82-93bb940a43de"},"_deposit":{"id":"16507","pid":{"type":"depid","value":"16507","revision_id":0},"owners":[1],"status":"published","created_by":1},"item_title":"Sub-Computation Based Transition Predicate Abstraction","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Sub-Computation Based Transition Predicate Abstraction"},{"subitem_title":"Sub-Computation Based Transition Predicate Abstraction","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"通常論文","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2007-06-15","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"Department of Computer Science  Graduate School of Information Science and Technology  the University of Tokyo"},{"subitem_text_value":"Department of Computer Science  Graduate School of Information Science and Technology  the University of Tokyo"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Department of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo","subitem_text_language":"en"},{"subitem_text_value":"Department of Computer Science, Graduate School of Information Science and Technology, the University of Tokyo","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/16507/files/IPSJ-TPRO4810009.pdf"},"date":[{"dateType":"Available","dateValue":"2009-06-15"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO4810009.pdf","filesize":[{"value":"465.3 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"660","billingrole":"5"},{"tax":["include_tax"],"price":"330","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"8510fcd5-d474-4a66-bac2-1cb7931b8d4f","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2007 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"CarlChristianFrederiksen"},{"creatorName":"Masami, Hagiya"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Carl, ChristianFrederiksen","creatorNameLang":"en"},{"creatorName":"Masami, Hagiya","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"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.","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"137","bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicPageStart":"114","bibliographicIssueDates":{"bibliographicIssueDate":"2007-06-15","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"SIG10(PRO33)","bibliographicVolumeNumber":"48"}]},"relation_version_is_last":true,"weko_creator_id":"1"},"updated":"2025-01-22T23:49:48.502848+00:00","created":"2025-01-18T22:49:45.588365+00:00","id":16507}